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 }