Boogie:

* Added /mv flag as the start of a Boogie replacement for /cev
* Allow attributes on assume statements
* /mv looks for the assume-statement attribute :captureState with a string-literal argument

4 files changed, 40 insertions, 17 deletions

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 5117da09..35929311 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -2379,6 +2379,7 @@ namespace Microsoft.Boogie {
   }

 

   public abstract class PredicateCmd : Cmd {

+    public QKeyValue Attributes;

     public /*readonly--except in StandardVisitor*/ Expr/*!*/ Expr;

     [ContractInvariantMethod]

     void ObjectInvariant() {

@@ -2391,6 +2392,13 @@ namespace Microsoft.Boogie {
       Contract.Requires(expr != null);

       Expr = expr;

     }

+    public PredicateCmd(IToken/*!*/ tok, Expr/*!*/ expr, QKeyValue kv)

+      : base(tok) {

+      Contract.Requires(tok != null);

+      Contract.Requires(expr != null);

+      Expr = expr;

+      Attributes = kv;

+    }

     public override void Resolve(ResolutionContext rc) {

       //Contract.Requires(rc != null);

       Expr.Resolve(rc);

@@ -2458,8 +2466,6 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public QKeyValue Attributes;

-

     private MiningStrategy errorDataEnhanced;

     public MiningStrategy ErrorDataEnhanced {

       get {

@@ -2478,11 +2484,10 @@ namespace Microsoft.Boogie {
     }

 

     public AssertCmd(IToken/*!*/ tok, Expr/*!*/ expr, QKeyValue kv)

-      : base(tok, expr) {

+      : base(tok, expr, kv) {

       Contract.Requires(tok != null);

       Contract.Requires(expr != null);

       errorDataEnhanced = GenerateBoundVarMiningStrategy(expr);

-      Attributes = kv;

     }

 

     public override void Emit(TokenTextWriter stream, int level) {

@@ -2639,9 +2644,15 @@ namespace Microsoft.Boogie {
       Contract.Requires(tok != null);

       Contract.Requires(expr != null);

     }

+    public AssumeCmd(IToken/*!*/ tok, Expr/*!*/ expr, QKeyValue kv)

+      : base(tok, expr, kv) {

+      Contract.Requires(tok != null);

+      Contract.Requires(expr != null);

+    }

     public override void Emit(TokenTextWriter stream, int level) {

       //Contract.Requires(stream != null);

       stream.Write(this, level, "assume ");

+      EmitAttributes(stream, Attributes);

       this.Expr.Emit(stream);

       stream.WriteLine(";");

     }

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index 132dfcbb..ed54c232 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -817,10 +817,11 @@ LabelOrCmd<out Cmd c, out IToken label>
   ( LabelOrAssign<out c, out label>

   | "assert"              (. x = t; .)

     { Attribute<ref kv> }

-    Proposition<out e>    (. c = new AssertCmd(x,e, kv); .)

+    Proposition<out e>    (. c = new AssertCmd(x, e, kv); .)

     ";"

   | "assume"              (. x = t; .)

-    Proposition<out e>    (. c = new AssumeCmd(x,e); .)

+    { Attribute<ref kv> }

+    Proposition<out e>    (. c = new AssumeCmd(x, e, kv); .)

     ";"

   | "havoc"               (. x = t; .)

     Idents<out xs> ";"    (. ids = new IdentifierExprSeq();

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index eadd8b97..4196670f 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -192,6 +192,7 @@ namespace Microsoft.Boogie {
       Contract.Invariant(-1 <= LoopFrameConditions && LoopFrameConditions < 3);

       Contract.Invariant(0 <= ModifiesDefault && ModifiesDefault < 7);

       Contract.Invariant((0 <= PrintErrorModel && PrintErrorModel <= 2) || PrintErrorModel == 4);

+      Contract.Invariant(0 <= ModelView && ModelView < 2);

       Contract.Invariant(0 <= EnhancedErrorMessages && EnhancedErrorMessages < 2);

       Contract.Invariant(0 <= StepsBeforeWidening && StepsBeforeWidening <= 9);

       Contract.Invariant(-1 <= BracketIdsInVC && BracketIdsInVC <= 1);

@@ -229,6 +230,7 @@ namespace Microsoft.Boogie {
     public int PrintErrorModel = 0;

     public string PrintErrorModelFile = null;

     public bool CEVPrint = false;

+    public int ModelView = 1;

     public int EnhancedErrorMessages = 0;

     public bool ForceBplErrors = false; // if true, boogie error is shown even if "msg" attribute is present

     public enum BvHandling {

@@ -918,6 +920,11 @@ namespace Microsoft.Boogie {
             CEVPrint = true;

             break;

 

+          case "-mv":

+          case "/mv":

+            ps.GetNumericArgument(ref ModelView, 2);

+            break;

+

           case "-printModelToFile":

           case "/printModelToFile":

             if (ps.ConfirmArgumentCount(1)) {

@@ -2029,6 +2036,7 @@ namespace Microsoft.Boogie {
                     4 - print Z3's error model in a more human readable way

   /printModelToFile:<file> : print model to <file> instead of console

   /cev:<file>       Print Z3's error model to <file> and include error message

+  /mv:<n>           0 - model view off, 1 (default) - model view on

   /enhancedErrorMessages:<n> : 0 (default) - no enhanced error messages

                                1 - Z3 error model enhanced error messages

 

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 98b1a7f9..a2887dcf 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -62,12 +62,12 @@ Contract.Requires(cce.NonNullElements(defines,true));
   return Parse(stream, filename, defines, out program);

 }

 

-

-public static int Parse(Stream stream, string/*!*/ filename, /*maybe null*/ List<string/*!*/> defines, out /*maybe null*/ Program program) /* throws System.IO.IOException */ {

-    Contract.Requires(stream != null);

-    Contract.Requires(filename != null);

-    Contract.Requires(cce.NonNullElements(defines, true));

   

+public static int Parse (Stream stream, string/*!*/ filename, /*maybe null*/ List<string/*!*/> defines, out /*maybe null*/ Program program) /* throws System.IO.IOException */ {

+Contract.Requires(stream != null);

+Contract.Requires(filename != null);

+Contract.Requires(cce.NonNullElements(defines,true));

+

   if (defines == null) {

     defines = new List<string/*!*/>();

   }

@@ -98,7 +98,7 @@ public static int Parse(Stream stream, string/*!*/ filename, /*maybe null*/ List
 private class BvBounds : Expr {

   public BigNum Lower;

   public BigNum Upper;

-  public BvBounds(IToken/*!*/ tok, BigNum lower, BigNum upper) :base(tok){//BASEMOVEA

+  public BvBounds(IToken/*!*/ tok, BigNum lower, BigNum upper) :base(tok){//BASEMOVE

     Contract.Requires(tok != null);

     //:base(tok);

     this.Lower = lower;

@@ -106,15 +106,15 @@ private class BvBounds : Expr {
   }

   public override Type/*!*/ ShallowType { get {Contract.Ensures(Contract.Result<Type>() != null); return Bpl.Type.Int; } }

   public override void Resolve(ResolutionContext/*!*/ rc) {

-  //Contract.Requires(rc != null);

+  Contract.Requires(rc != null);

     rc.Error(this, "bitvector bounds in illegal position");

   }

   public override void Emit(TokenTextWriter/*!*/ stream,

                             int contextBindingStrength, bool fragileContext) {

-    //Contract.Requires(stream != null);

+    Contract.Requires(stream != null);

     {Contract.Assert(false);throw new cce.UnreachableException();}

   }

-  public override void ComputeFreeVariables(Set/*!*/ freeVars) {/*Contract.Requires(freeVars != null);*/ {Contract.Assert(false);throw new cce.UnreachableException();} }

+  public override void ComputeFreeVariables(Set/*!*/ freeVars) {Contract.Requires(freeVars != null); {Contract.Assert(false);throw new cce.UnreachableException();} }

   public override AI.IExpr/*!*/ IExpr { get { Contract.Ensures(Contract.Result<AI.IExpr>()!=null); {Contract.Assert(false);throw new cce.UnreachableException();} } }

 }

 

@@ -979,13 +979,16 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 				Attribute(ref kv);

 			}

 			Proposition(out e);

-			c = new AssertCmd(x,e, kv); 

+			c = new AssertCmd(x, e, kv); 

 			Expect(7);

 		} else if (la.kind == 45) {

 			Get();

 			x = t; 

+			while (la.kind == 25) {

+				Attribute(ref kv);

+			}

 			Proposition(out e);

-			c = new AssumeCmd(x,e); 

+			c = new AssumeCmd(x, e, kv); 

 			Expect(7);

 		} else if (la.kind == 46) {

 			Get();