    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 /*@ 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    }