001    /* Copyright 2000, 2001, Compaq Computer Corporation */
002    
003    package escjava.prover;
004    
005    import escjava.translate.UniqName;
006    import javafe.util.Location;
007    
008    /**
009     * An object of this class represent a "result" produced by Simplify.
010     * 
011     * @see Simplify
012     * @see escjava.prover.CECEnum
013     * @see SExp
014     */
015    
016    public class TriggerlessQuantWarning extends SimplifyResult
017    {
018        public /*@ non_null @*/ SExp e0;
019    
020        int n;
021        //@ invariant 0 <= n;
022    
023        public /*@ non_null @*/ SExp e1;
024    
025        /*@ normal_behavior
026          @   requires 0 <= n;
027          @   modifies this.e0, this.n, this.e1;
028          @   ensures this.e0 == e0;
029          @   ensures this.n == n;
030          @   ensures this.e1 == e1;
031          @   ensures this.labels == labels;
032          @   ensures this.context == context;
033          @*/
034        TriggerlessQuantWarning(SList labels,
035                                SList context,
036                                /*@ non_null @*/ SExp e0,
037                                int n,
038                                /*@ non_null @*/ SExp e1) {
039            super(WARNING_TRIGGERLESS_QUANT, labels, context);
040            this.e0 = e0;
041            this.n = n;
042            this.e1 = e1;
043        }
044    
045        //@ also
046        //@ normal_behavior
047        //@   ensures \result != null;
048        public /*@ non_null pure @*/ String toString() {
049            return super.toString() + " e0=" + e0 + " n=" + n + " e1=" + e1;
050        }
051    
052        /**
053         * Attempts to glean a location from the name of the dummy
054         * variable appearing in <code>e1</code>.  If none can be
055         * retrieved, the <code>null</code> location is returned.
056         */
057        //@ normal_behavior
058        //@   ensures \result > 0 || \result == Location.NULL;
059        public /*@ pure @*/ int getLocation() {
060            try {
061                SList quant = e1.getList();
062                if (quant.length() < 2 || ! quant.at(0).toString().equals("FORALL")) {
063                    return Location.NULL;
064                }
065                SList dummies = quant.at(1).getList();
066                String dummy = dummies.at(0).getAtom().toString();
067    
068                int k = dummy.indexOf(':');
069                if (k == -1) {
070                    return Location.NULL;
071                }
072                return UniqName.suffixToLoc(dummy.substring(k+1), true);
073    
074            } catch (SExpTypeError sete) {
075                return Location.NULL;
076            }
077        }
078    }