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

16 files changed, 282 insertions, 143 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index a0005263..b4798299 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -731,6 +731,9 @@ namespace Microsoft.Boogie {
                     Console.WriteLine("Execution trace:");

                     error.Print(4);

                   }

+                  if (CommandLineOptions.Clo.ModelView == 1) {

+                    error.PrintModel();

+                  }

                   errorCount++;

                 }

                 //}

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();

diff --git a/Source/Provers/Simplify/Prover.cs b/Source/Provers/Simplify/Prover.cs
index d49b10e1..3faa18e1 100644
--- a/Source/Provers/Simplify/Prover.cs
+++ b/Source/Provers/Simplify/Prover.cs
@@ -55,16 +55,17 @@ namespace Microsoft.Boogie.Simplify {
         //modifies this.*;

       {

         Contract.Requires(cce.IsPeerConsistent(this));

-        cce.BeginExpose(this);

-        {

+        try {

+          cce.BeginExpose(this);

           simplify.Refresh();

 #if WHIDBEY

             return simplify.PeakVirtualMemorySize64;

 #else

           return simplify.PeakPagedMemorySize64;

 #endif

+        } finally {

+          cce.EndExpose();

         }

-        cce.EndExpose();

       }

     }

 

@@ -333,11 +334,12 @@ namespace Microsoft.Boogie.Simplify {
     protected int FromReadChar()

       //modifies this.*;

     {

-      cce.BeginExpose(this);

-      {

+      try {

+        cce.BeginExpose(this);

         return fromSimplify.Read();

+      } finally {

+        cce.EndExpose();

       }

-      cce.EndExpose();

     }

 

     private void KillProver(object state) {

@@ -353,32 +355,34 @@ namespace Microsoft.Boogie.Simplify {
       //modifies this.*;

     {

       Contract.Requires(-1 <= timeout);

-      cce.BeginExpose(this);

-      {

+      try {

+        cce.BeginExpose(this);

         this.readTimedOut = false;

         System.Threading.Timer t = new System.Threading.Timer(this.KillProver, null, timeout, System.Threading.Timeout.Infinite);

         int ch = fromSimplify.Read();

         t.Change(System.Threading.Timeout.Infinite, System.Threading.Timeout.Infinite);

         t.Dispose();

         return ch;

+      } finally {

+        cce.EndExpose();

       }

-      cce.EndExpose();

     }

 

     protected string FromReadLine()

       //modifies this.*;

     {

       Contract.Ensures(Contract.Result<string>() != null);

-      cce.BeginExpose(this);

-      {

+      try {

+        cce.BeginExpose(this);

         string s = fromSimplify.ReadLine();

         if (s == null) {

           // this is what ReadLine returns if all characters have been read

           s = "";

         }

         return s;

+      } finally {

+        cce.EndExpose();

       }

-      cce.EndExpose();

     }

 

     protected string FromStdErrorAll()

@@ -386,8 +390,8 @@ namespace Microsoft.Boogie.Simplify {
     {

       Contract.Ensures(Contract.Result<string>() != null);

 

-      cce.BeginExpose(this);

-      {

+      try {

+        cce.BeginExpose(this);

         if (fromStdError != null) {

           string s = fromStdError.ReadToEnd();

           if (s == null) {

@@ -395,13 +399,13 @@ namespace Microsoft.Boogie.Simplify {
             s = "";

           }

           return s;

-        }

+        } else {

           // there is no StdErrorReader available

-        else {

           return "";

         }

+      } finally {

+        cce.EndExpose();

       }

-      cce.EndExpose();

     }

 

     protected void ToWriteLine(string s)

diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs
index a36ca87a..33e622ba 100644
--- a/Source/Provers/Z3/Prover.cs
+++ b/Source/Provers/Z3/Prover.cs
@@ -70,6 +70,7 @@ namespace Microsoft.Boogie.Z3
     {

       return CommandLineOptions.Clo.PrintErrorModel >= 1 ||

              CommandLineOptions.Clo.EnhancedErrorMessages == 1 ||

+             CommandLineOptions.Clo.ModelView > 0 ||

              CommandLineOptions.Clo.ContractInfer ||

              CommandLineOptions.Clo.LazyInlining > 0 ||

              CommandLineOptions.Clo.StratifiedInlining > 0;

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index d30c93e9..85e0c963 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -360,7 +360,7 @@ namespace Microsoft.Boogie {
     }

 

     public int LookupPartitionValue(int partition) {

-      BigNum bignum = (BigNum)cce.NonNull(partitionToValue)[partition];

+      BigNum bignum = (BigNum)cce.NonNull(partitionToValue[partition]);

       return bignum.ToInt;

     }

 

@@ -377,7 +377,6 @@ namespace Microsoft.Boogie {
       }

       Contract.Assert(false);

       throw new cce.UnreachableException();

-      return 0;

     }

 

     private string LookupSkolemConstant(string name) {

@@ -440,7 +439,6 @@ namespace Microsoft.Boogie {
       }

       Contract.Assert(false);

       throw new cce.UnreachableException();

-      return 0;

     }

 

     public List<object>/*!>!*/ PartitionsToValues(List<int> args) {

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index dc13725f..aac288b9 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -75,17 +75,20 @@ namespace Microsoft.Boogie {
 

     [Peer]

     public BlockSeq Trace;

+    public ErrorModel Model;

+    public VC.ModelViewInfo MvInfo;

     [Peer]

     public List<string>/*!>!*/ relatedInformation;

 

     public Dictionary<TraceLocation, CalleeCounterexampleInfo> calleeCounterexamples;

 

-    internal Counterexample(BlockSeq trace) {

+    internal Counterexample(BlockSeq trace, ErrorModel model, VC.ModelViewInfo mvInfo) {

       Contract.Requires(trace != null);

       this.Trace = trace;

+      this.Model = model;

+      this.MvInfo = mvInfo;

       this.relatedInformation = new List<string>();

       this.calleeCounterexamples = new Dictionary<TraceLocation, CalleeCounterexampleInfo>();

-      // base();

     }

 

     // Create a shallow copy of the counterexample

@@ -140,34 +143,29 @@ namespace Microsoft.Boogie {
         return naryExpr.Fun.FunctionName;

     }

 

-    public void Print(int spaces) {

+    public void Print(int indent) {

       int numBlock = -1;

+      string ind = new string(' ', indent);

       foreach (Block b in Trace) {

         Contract.Assert(b != null);

         numBlock++;

         if (b.tok == null) {

-          Console.WriteLine("    <intermediate block>");

+          Console.WriteLine("{0}<intermediate block>", ind);

         } else {

           // for ErrorTrace == 1 restrict the output;

           // do not print tokens with -17:-4 as their location because they have been 

           // introduced in the translation and do not give any useful feedback to the user

           if (!(CommandLineOptions.Clo.ErrorTrace == 1 && b.tok.line == -17 && b.tok.col == -4)) {

-            for (int i = 0; i < spaces + 4; i++)

-              Console.Write(" ");

-            Console.WriteLine("{0}({1},{2}): {3}", b.tok.filename, b.tok.line, b.tok.col, b.Label);

+            Console.WriteLine("{4}{0}({1},{2}): {3}", b.tok.filename, b.tok.line, b.tok.col, b.Label, ind);

             for (int numInstr = 0; numInstr < b.Cmds.Length; numInstr++)

             {

                 var loc = new TraceLocation(numBlock, numInstr);

                 if (calleeCounterexamples.ContainsKey(loc))

                 {

                     var cmd = getTraceCmd(loc);

-                    for (int i = 0; i < spaces + 4; i++)

-                        Console.Write(" ");

-                    Console.WriteLine("Inlined call to procedure {0} begins", getCalledProcName(cmd));

-                    calleeCounterexamples[loc].counterexample.Print(spaces + 4);

-                    for (int i = 0; i < spaces + 4; i++)

-                        Console.Write(" ");

-                    Console.WriteLine("Inlined call to procedure {0} ends", getCalledProcName(cmd));

+                    Console.WriteLine("{1}Inlined call to procedure {0} begins", getCalledProcName(cmd), ind);

+                    calleeCounterexamples[loc].counterexample.Print(indent + 4);

+                    Console.WriteLine("{1}Inlined call to procedure {0} ends", getCalledProcName(cmd), ind);

                 }

             }

           }

@@ -175,6 +173,38 @@ namespace Microsoft.Boogie {
       }

     }

 

+    public void PrintModel() {

+      if (Model == null || MvInfo == null) {

+        return;

+      }

+      if (!Model.definedFunctions.ContainsKey("@MV_state")) {

+        return;

+      }

+      Console.WriteLine("Captured states:");

+      List<List<int>> defs = Model.definedFunctions["@MV_state"];

+      List<int> states = new List<int>();

+      foreach (List<int> parameters in defs) {

+        if (parameters.Count == 2) {  // we expect this for all but possibly the last row

+          int argPartition = parameters[0];

+          object val = Model.partitionToValue[argPartition];

+          if (val is BigNum) {

+            BigNum n = (BigNum)val;

+            states.Add(n.ToInt);

+          }

+        }

+      }

+      // we now have the list of states in 'states'

+      states.Sort();

+      foreach (int s in states) {

+        if (0 <= s && s < MvInfo.Info.Count) {

+          VC.ModelViewInfo.Mapping m = MvInfo.Info[s];

+          Console.WriteLine("    {0}", m.Description);

+        } else {

+          Console.WriteLine("    undefined captured-state ID {0}", s);

+        }

+      }

+    }

+

     public abstract int GetLocation();

   }

 

@@ -199,8 +229,8 @@ namespace Microsoft.Boogie {
     }

 

 

-    public AssertCounterexample(BlockSeq trace, AssertCmd failingAssert)

-      : base(trace) {

+    public AssertCounterexample(BlockSeq trace, AssertCmd failingAssert, ErrorModel model, VC.ModelViewInfo mvInfo)

+      : base(trace, model, mvInfo) {

       Contract.Requires(trace != null);

       Contract.Requires(failingAssert != null);

       this.FailingAssert = failingAssert;

@@ -213,7 +243,7 @@ namespace Microsoft.Boogie {
 

     public override Counterexample Clone()

     {

-        var ret = new AssertCounterexample(Trace, FailingAssert);

+        var ret = new AssertCounterexample(Trace, FailingAssert, Model, MvInfo);

         ret.calleeCounterexamples = calleeCounterexamples;

         return ret;

     }

@@ -229,8 +259,8 @@ namespace Microsoft.Boogie {
     }

 

 

-    public CallCounterexample(BlockSeq trace, CallCmd failingCall, Requires failingRequires)

-      : base(trace) {

+    public CallCounterexample(BlockSeq trace, CallCmd failingCall, Requires failingRequires, ErrorModel model, VC.ModelViewInfo mvInfo)

+      : base(trace, model, mvInfo) {

       Contract.Requires(!failingRequires.Free);

       Contract.Requires(trace != null);

       Contract.Requires(failingCall != null);

@@ -246,7 +276,7 @@ namespace Microsoft.Boogie {
 

     public override Counterexample Clone()

     {

-        var ret = new CallCounterexample(Trace, FailingCall, FailingRequires);

+        var ret = new CallCounterexample(Trace, FailingCall, FailingRequires, Model, MvInfo);

         ret.calleeCounterexamples = calleeCounterexamples;

         return ret;

     }

@@ -262,8 +292,8 @@ namespace Microsoft.Boogie {
     }

 

 

-    public ReturnCounterexample(BlockSeq trace, TransferCmd failingReturn, Ensures failingEnsures)

-      : base(trace) {

+    public ReturnCounterexample(BlockSeq trace, TransferCmd failingReturn, Ensures failingEnsures, ErrorModel model, VC.ModelViewInfo mvInfo)

+      : base(trace, model, mvInfo) {

       Contract.Requires(trace != null);

       Contract.Requires(failingReturn != null);

       Contract.Requires(failingEnsures != null);

@@ -279,7 +309,7 @@ namespace Microsoft.Boogie {
 

     public override Counterexample Clone()

     {

-        var ret = new ReturnCounterexample(Trace, FailingReturn, FailingEnsures);

+        var ret = new ReturnCounterexample(Trace, FailingReturn, FailingEnsures, Model, MvInfo);

         ret.calleeCounterexamples = calleeCounterexamples;

         return ret;

     }

@@ -1081,16 +1111,17 @@ namespace VC {
 

     Hashtable preHavocIncarnationMap = null;     // null = the previous command was not an HashCmd. Otherwise, a *copy* of the map before the havoc statement

 

-    protected void TurnIntoPassiveBlock(Block b, Hashtable /*Variable -> Expr*/ incarnationMap, Substitution oldFrameSubst) {

+    protected void TurnIntoPassiveBlock(Block b, Hashtable /*Variable -> Expr*/ incarnationMap, ModelViewInfo mvInfo, Substitution oldFrameSubst) {

       Contract.Requires(b != null);

       Contract.Requires(incarnationMap != null);

+      Contract.Requires(mvInfo != null);

       Contract.Requires(oldFrameSubst != null);

       #region Walk forward over the commands in this block and convert them to passive commands

 

       CmdSeq passiveCmds = new CmdSeq();

       foreach (Cmd c in b.Cmds) {

         Contract.Assert(c != null); // walk forward over the commands because the map gets modified in a forward direction      

-        TurnIntoPassiveCmd(c, incarnationMap, oldFrameSubst, passiveCmds);

+        TurnIntoPassiveCmd(c, incarnationMap, oldFrameSubst, passiveCmds, mvInfo);

       }

       b.Cmds = passiveCmds;

 

@@ -1103,10 +1134,10 @@ namespace VC {
       #endregion

     }

 

-    protected Hashtable /*Variable -> Expr*/ Convert2PassiveCmd(Implementation impl) {

+    protected Hashtable /*Variable -> Expr*/ Convert2PassiveCmd(Implementation impl, out ModelViewInfo mvInfo) {

       Contract.Requires(impl != null);

 

-      Hashtable r = ConvertBlocks2PassiveCmd(impl.Blocks, impl.Proc.Modifies);

+      Hashtable r = ConvertBlocks2PassiveCmd(impl.Blocks, impl.Proc.Modifies, out mvInfo);

 

       RestoreParamWhereClauses(impl);

 

@@ -1120,7 +1151,7 @@ namespace VC {
       return r;

     }

 

-    protected Hashtable /*Variable -> Expr*/ ConvertBlocks2PassiveCmd(List<Block> blocks, IdentifierExprSeq modifies) {

+    protected Hashtable /*Variable -> Expr*/ ConvertBlocks2PassiveCmd(List<Block> blocks, IdentifierExprSeq modifies, out ModelViewInfo mvInfo) {

       Contract.Requires(blocks != null);

       Contract.Requires(modifies != null);

       #region Convert to Passive Commands

@@ -1155,6 +1186,7 @@ namespace VC {
       // processed all of a node's predecessors before we process the node.

       Hashtable /*Block -> IncarnationMap*/ block2Incarnation = new Hashtable/*Block -> IncarnationMap*/();

       Block exitBlock = null;

+      mvInfo = new ModelViewInfo();

       foreach (Block b in sortedNodes) {

         Contract.Assert(b != null);

         Contract.Assert(!block2Incarnation.Contains(b));

@@ -1164,7 +1196,7 @@ namespace VC {
         block2Incarnation.Add(b, incarnationMap);

         #endregion Each block's map needs to be available to successor blocks

 

-        TurnIntoPassiveBlock(b, incarnationMap, oldFrameSubst);

+        TurnIntoPassiveBlock(b, incarnationMap, mvInfo, oldFrameSubst);

         exitBlock = b;

       }

 

@@ -1177,13 +1209,15 @@ namespace VC {
     }

 

     /// <summary> 

-    /// Turn a command into a passive command, and it remembers the previous step, to see if it is a havoc or not. In the case, it remebers the incarnation map BEFORE the havoc

+    /// Turn a command into a passive command, and it remembers the previous step, to see if it is a havoc or not. In the case, it remembers the incarnation map BEFORE the havoc

+    /// Meanwhile, record any information needed to later reconstruct a model view.

     /// </summary> 

-    protected void TurnIntoPassiveCmd(Cmd c, Hashtable /*Variable -> Expr*/ incarnationMap, Substitution oldFrameSubst, CmdSeq passiveCmds) {

+    protected void TurnIntoPassiveCmd(Cmd c, Hashtable /*Variable -> Expr*/ incarnationMap, Substitution oldFrameSubst, CmdSeq passiveCmds, ModelViewInfo mvInfo) {

       Contract.Requires(c != null);

       Contract.Requires(incarnationMap != null);

       Contract.Requires(oldFrameSubst != null);

       Contract.Requires(passiveCmds != null);

+      Contract.Requires(mvInfo != null);

       Substitution incarnationSubst = Substituter.SubstitutionFromHashtable(incarnationMap);

       #region assert/assume P |--> assert/assume P[x := in(x)], out := in

       if (c is PredicateCmd) {

@@ -1193,6 +1227,14 @@ namespace VC {
         Contract.Assert(pc != null);

 

         Expr copy = Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, pc.Expr);

+        if (0 < CommandLineOptions.Clo.ModelView && pc is AssumeCmd) {

+          string description = QKeyValue.FindStringAttribute(pc.Attributes, "captureState");

+          if (description != null) {

+            Expr mv = new NAryExpr(pc.tok, new FunctionCall(mvInfo.MVState), new ExprSeq(Bpl.Expr.Literal(mvInfo.Info.Count)));

+            copy = Bpl.Expr.And(mv, copy);

+            mvInfo.Info.Add(new ModelViewInfo.Mapping(description, incarnationMap));

+          }

+        }

         Contract.Assert(copy != null);

         if (pc is AssertCmd) {

           ((AssertCmd)pc).OrigExpr = pc.Expr;

@@ -1312,7 +1354,7 @@ namespace VC {
         Contract.Assert(sug != null);

         Cmd cmd = sug.Desugaring;

         Contract.Assert(cmd != null);

-        TurnIntoPassiveCmd(cmd, incarnationMap, oldFrameSubst, passiveCmds);

+        TurnIntoPassiveCmd(cmd, incarnationMap, oldFrameSubst, passiveCmds, mvInfo);

       } else if (c is StateCmd) {

         this.preHavocIncarnationMap = null;       // we do not need to remeber the previous incarnations

         StateCmd st = (StateCmd)c;

@@ -1328,7 +1370,7 @@ namespace VC {
         // do the sub-commands

         foreach (Cmd s in st.Cmds) {

           Contract.Assert(s != null);

-          TurnIntoPassiveCmd(s, incarnationMap, oldFrameSubst, passiveCmds);

+          TurnIntoPassiveCmd(s, incarnationMap, oldFrameSubst, passiveCmds, mvInfo);

         }

         // remove the local variables from the incarnation map

         foreach (Variable v in st.Locals) {

@@ -1343,7 +1385,7 @@ namespace VC {
       #endregion

 

 

-      #region We rember if we have put an havoc statement into a passive form

+      #region We remember if we have put an havoc statement into a passive form

 

       if (!(c is HavocCmd))

         this.preHavocIncarnationMap = null;

@@ -1434,4 +1476,22 @@ namespace VC {
     }

 

   }

+

+  public class ModelViewInfo

+  {

+    public readonly List<Mapping> Info = new List<Mapping>();

+    public readonly Function MVState = new Function(Token.NoToken, "@MV_state",

+      new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Int), true)),

+      new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Bool), false));

+

+    public class Mapping

+    {

+      public readonly string Description;

+      public readonly Hashtable /*Variable -> Expr*/ IncarnationMap;

+      public Mapping(string description, Hashtable /*Variable -> Expr*/ incarnationMap) {

+        Description = description;

+        IncarnationMap = incarnationMap;

+      }

+    }

+  }

 }

diff --git a/Source/VCGeneration/DoomCheck.cs b/Source/VCGeneration/DoomCheck.cs
index 2407fecf..62b0833c 100644
--- a/Source/VCGeneration/DoomCheck.cs
+++ b/Source/VCGeneration/DoomCheck.cs
@@ -174,7 +174,6 @@ void ObjectInvariant()
             #endregion

 

        */ 

-        private bool _tmpUseFreshBVars;

        

         VCExpr GenerateEVC(Implementation impl, out Hashtable label2absy, Checker ch)

         {

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index c6e77b67..80934bc2 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -216,7 +216,8 @@ namespace VC {
 

       Implementation impl = info.impl;

       ConvertCFG2DAG(impl, program);

-      info.gotoCmdOrigins = PassifyImpl(impl, program);

+      ModelViewInfo mvInfo;

+      info.gotoCmdOrigins = PassifyImpl(impl, program, out mvInfo);

       Contract.Assert(info.exitIncarnationMap != null);

       Hashtable/*<int, Absy!>*/ label2absy;

       VCExpressionGenerator gen = checker.VCExprGen;

@@ -361,7 +362,8 @@ namespace VC {
       Implementation impl = info.impl;

       Contract.Assert(impl != null);

       ConvertCFG2DAG(impl, program);

-      info.gotoCmdOrigins = PassifyImpl(impl, program);

+      ModelViewInfo mvInfo;

+      info.gotoCmdOrigins = PassifyImpl(impl, program, out mvInfo);

       Contract.Assert(info.exitIncarnationMap != null);

       Hashtable/*<int, Absy!>*/ label2absy;

       VCExpressionGenerator gen = checker.VCExprGen;

@@ -646,7 +648,8 @@ namespace VC {
           Emit();

         }

         parent.CurrentLocalVariables = impl.LocVars;

-        parent.PassifyImpl(impl, program);

+        ModelViewInfo mvInfo;

+        parent.PassifyImpl(impl, program, out mvInfo);

         Hashtable label2Absy;

         Checker ch = parent.FindCheckerFor(impl, CommandLineOptions.Clo.SmokeTimeout);

         Contract.Assert(ch != null);

@@ -711,9 +714,11 @@ namespace VC {
             if (IsFalse(assrt.Expr))

               return;

 

+#if TURN_ASSERT_INFO_ASSUMES

             if (turnAssertIntoAssumes) {

               cmd = AssertTurnedIntoAssume(assrt);

             }

+#endif

           } else if (assm != null) {

             if (IsFalse(assm.Expr))

               assumeFalse = true;

@@ -848,7 +853,6 @@ namespace VC {
       Block split_block;

       bool assert_to_assume;

       List<Block/*!*/>/*!*/ assumized_branches = new List<Block/*!*/>();

-      public AssertCmd/*?*/ first_assert;

 

       double score;

       bool score_computed;

@@ -1371,7 +1375,7 @@ namespace VC {
           foreach (Cmd c in b.Cmds) {

             Contract.Assert(c != null);

             if (c is AssertCmd) {

-              return AssertCmdToCounterexample((AssertCmd)c, cce.NonNull(b.TransferCmd), trace, null, new Dictionary<Incarnation, Absy>());

+              return AssertCmdToCounterexample((AssertCmd)c, cce.NonNull(b.TransferCmd), trace, null, null, new Dictionary<Incarnation, Absy>());

             }

           }

         }

@@ -1529,7 +1533,7 @@ namespace VC {
         }

       }

 

-      public void BeginCheck(VerifierCallback callback, int no, int timeout) {

+      public void BeginCheck(VerifierCallback callback, ModelViewInfo mvInfo, int no, int timeout) {

         Contract.Requires(callback != null);

         splitNo = no;

 

@@ -1552,7 +1556,8 @@ namespace VC {
 

             vcgen.ComputePredecessors(codeExpr.Blocks);

             vcgen.AddBlocksBetween(codeExpr.Blocks);

-            Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = vcgen.ConvertBlocks2PassiveCmd(codeExpr.Blocks, new IdentifierExprSeq());

+            ModelViewInfo mvInfoCodeExpr;

+            Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = vcgen.ConvertBlocks2PassiveCmd(codeExpr.Blocks, new IdentifierExprSeq(), out mvInfoCodeExpr);

             VCExpr startCorrect = VCGen.LetVC(

 		      codeExpr.Blocks[0],

               null,

@@ -1585,9 +1590,9 @@ namespace VC {
         Contract.Assert(vc != null);

 

         if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) {

-          reporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback, parent.implName2LazyInliningInfo, cce.NonNull(this.Checker.TheoremProver.Context), parent.program);

+          reporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback, mvInfo, parent.implName2LazyInliningInfo, cce.NonNull(this.Checker.TheoremProver.Context), parent.program);

         } else {

-          reporter = new ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback, parent.implName2LazyInliningInfo, this.Checker.TheoremProver.Context, parent.program);

+          reporter = new ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback, mvInfo, parent.implName2LazyInliningInfo, this.Checker.TheoremProver.Context, parent.program);

         }

 

         if (CommandLineOptions.Clo.TraceVerify && no >= 0) {

@@ -1743,7 +1748,8 @@ namespace VC {
         smoke_tester.Copy();

       }

 

-      Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = PassifyImpl(impl, program);

+      ModelViewInfo mvInfo;

+      Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = PassifyImpl(impl, program, out mvInfo);

 

       double max_vc_cost = CommandLineOptions.Clo.VcsMaxCost;

       int tmp_max_vc_cost = -1, max_splits = CommandLineOptions.Clo.VcsMaxSplits, 

@@ -1791,7 +1797,7 @@ namespace VC {
             }

             callback.OnProgress("VCprove", no < 0 ? 0 : no, total, proven_cost / (remaining_cost + proven_cost));

 

-            s.BeginCheck(callback, no, 

+            s.BeginCheck(callback, mvInfo, no, 

               (keep_going && s.LastChance) ? CommandLineOptions.Clo.VcsFinalAssertTimeout :

                 keep_going ? CommandLineOptions.Clo.VcsKeepGoingTimeout :

                              CommandLineOptions.Clo.ProverKillTime);

@@ -1950,7 +1956,7 @@ namespace VC {
                {

                    coverageProcess.Start();

                }

-               catch (System.ComponentModel.Win32Exception e)

+               catch (System.ComponentModel.Win32Exception)

                {

                    coverageProcess.Dispose();

                    coverageProcess = null;

@@ -2472,7 +2478,8 @@ namespace VC {
       Contract.Ensures(Contract.ValueAtReturn(out reporter) != null);

 

       ConvertCFG2DAG(impl, program);

-      Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = PassifyImpl(impl, program);

+      ModelViewInfo mvInfo;

+      Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = PassifyImpl(impl, program, out mvInfo);

       Checker checker = FindCheckerFor(impl, CommandLineOptions.Clo.ProverKillTime);

       Contract.Assert(checker != null);

 

@@ -2488,7 +2495,7 @@ namespace VC {
       */

 

       reporter = new StratifiedInliningErrorReporter(

-         cce.NonNull(implName2StratifiedInliningInfo), checker.TheoremProver, callback,

+         cce.NonNull(implName2StratifiedInliningInfo), checker.TheoremProver, callback, mvInfo,

          checker.TheoremProver.Context, gotoCmdOrigins, program, impl);

 

     }

@@ -2944,6 +2951,7 @@ namespace VC {
       List<Block/*!*/>/*!*/ blocks;

       protected Dictionary<Incarnation, Absy/*!*/>/*!*/ incarnationOriginMap;

       protected VerifierCallback/*!*/ callback;

+      protected ModelViewInfo MvInfo;

       internal string resourceExceededMessage;

       static System.IO.TextWriter modelWriter;

       [ContractInvariantMethod]

@@ -2978,6 +2986,7 @@ namespace VC {
           List<Block/*!*/>/*!*/ blocks,

           Dictionary<Incarnation, Absy/*!*/>/*!*/ incarnationOriginMap,

           VerifierCallback/*!*/ callback,

+          ModelViewInfo mvInfo,

           Dictionary<string/*!*/, LazyInliningInfo/*!*/>/*!*/ implName2LazyInliningInfo,

           ProverContext/*!*/ context,

           Program/*!*/ program) {

@@ -2994,6 +3003,7 @@ namespace VC {
         this.blocks = blocks;

         this.incarnationOriginMap = incarnationOriginMap;

         this.callback = callback;

+        this.MvInfo = mvInfo;

 

         this.implName2LazyInliningInfo = implName2LazyInliningInfo;

         this.context = context;

@@ -3004,10 +3014,10 @@ namespace VC {
       public override void OnModel(IList<string/*!*/>/*!*/ labels, ErrorModel errModel) {

         //Contract.Requires(cce.NonNullElements(labels));

         if (CommandLineOptions.Clo.PrintErrorModel >= 1 && errModel != null) {

-            if (VC.ConditionGeneration.errorModelList != null)

-            {

-                VC.ConditionGeneration.errorModelList.Add(errModel);

-            }

+          if (VC.ConditionGeneration.errorModelList != null)

+          {

+            VC.ConditionGeneration.errorModelList.Add(errModel);

+          }

           errModel.Print(ErrorReporter.ModelWriter);

           ErrorReporter.ModelWriter.Flush();

         }

@@ -3027,7 +3037,7 @@ namespace VC {
         Contract.Assert(traceNodes.Contains(entryBlock));

         trace.Add(entryBlock);

 

-        Counterexample newCounterexample = TraceCounterexample(entryBlock, traceNodes, trace, errModel, incarnationOriginMap, implName2LazyInliningInfo, context, program, new Dictionary<TraceLocation, CalleeCounterexampleInfo>());

+        Counterexample newCounterexample = TraceCounterexample(entryBlock, traceNodes, trace, errModel, MvInfo, incarnationOriginMap, implName2LazyInliningInfo, context, program, new Dictionary<TraceLocation, CalleeCounterexampleInfo>());

 

         if (newCounterexample == null)

           return;

@@ -3074,10 +3084,11 @@ namespace VC {
           List<Block/*!*/>/*!*/ blocks,

           Dictionary<Incarnation, Absy/*!*/>/*!*/ incarnationOriginMap,

           VerifierCallback/*!*/ callback,

+          ModelViewInfo mvInfo,

           Dictionary<string/*!*/, LazyInliningInfo/*!*/>/*!*/ implName2LazyInliningInfo,

           ProverContext/*!*/ context,

           Program/*!*/ program)

-        : base(gotoCmdOrigins, label2absy, blocks, incarnationOriginMap, callback, implName2LazyInliningInfo, context, program) // here for aesthetic purposes //TODO: Maybe nix?

+        : base(gotoCmdOrigins, label2absy, blocks, incarnationOriginMap, callback, mvInfo, implName2LazyInliningInfo, context, program) // here for aesthetic purposes //TODO: Maybe nix?

       {

         Contract.Requires(gotoCmdOrigins != null);

         Contract.Requires(label2absy != null);

@@ -3122,7 +3133,7 @@ namespace VC {
             if (b.Cmds.Has(a)) {

               BlockSeq trace = new BlockSeq();

               trace.Add(b);

-              Counterexample newCounterexample = AssertCmdToCounterexample(a, cce.NonNull(b.TransferCmd), trace, errModel, incarnationOriginMap);

+              Counterexample newCounterexample = AssertCmdToCounterexample(a, cce.NonNull(b.TransferCmd), trace, errModel, MvInfo, incarnationOriginMap);

               callback.OnCounterexample(newCounterexample, null);

               goto NEXT_ASSERT;

             }

@@ -3139,6 +3150,7 @@ namespace VC {
       Dictionary<string/*!*/, StratifiedInliningInfo/*!*/>/*!*/ implName2StratifiedInliningInfo;

       ProverInterface/*!*/ theoremProver;

       VerifierCallback/*!*/ callback;

+      ModelViewInfo mvInfo;

       FCallHandler calls;

       Program/*!*/ program;

       Implementation/*!*/ mainImpl;

@@ -3161,7 +3173,7 @@ namespace VC {
 

 

       public StratifiedInliningErrorReporter(Dictionary<string/*!*/, StratifiedInliningInfo/*!*/>/*!*/ implName2StratifiedInliningInfo,

-                                             ProverInterface/*!*/ theoremProver, VerifierCallback/*!*/ callback, ProverContext/*!*/ context,

+                                             ProverInterface/*!*/ theoremProver, VerifierCallback/*!*/ callback, ModelViewInfo mvInfo, ProverContext/*!*/ context,

                                              Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins,

                                              Program/*!*/ program, Implementation/*!*/ mainImpl) {

         Contract.Requires(cce.NonNullElements(implName2StratifiedInliningInfo));

@@ -3172,6 +3184,7 @@ namespace VC {
         this.implName2StratifiedInliningInfo = implName2StratifiedInliningInfo;

         this.theoremProver = theoremProver;

         this.callback = callback;

+        this.mvInfo = mvInfo;

         this.context = context;

         this.program = program;

         this.mainImpl = mainImpl;

@@ -3191,7 +3204,7 @@ namespace VC {
         if (underapproximationMode) {

           if (errModel == null)

             return;

-          GenerateTraceMain(labels, errModel);

+          GenerateTraceMain(labels, errModel, mvInfo);

           return;

         }

 

@@ -3212,7 +3225,7 @@ namespace VC {
       }

 

       // Construct the interprocedural trace

-      private void GenerateTraceMain(IList<string/*!*/>/*!*/ labels, ErrorModel/*!*/ errModel) {

+      private void GenerateTraceMain(IList<string/*!*/>/*!*/ labels, ErrorModel/*!*/ errModel, ModelViewInfo mvInfo) {

         Contract.Requires(errModel != null);

         Contract.Requires(cce.NonNullElements(labels));

         if (CommandLineOptions.Clo.PrintErrorModel >= 1 && errModel != null) {

@@ -3221,7 +3234,7 @@ namespace VC {
         }

 

         Counterexample newCounterexample =

-          GenerateTrace(labels, errModel, 0, mainImpl);

+          GenerateTrace(labels, errModel, mvInfo, 0, mainImpl);

 

         if (newCounterexample == null)

           return;

@@ -3244,7 +3257,7 @@ namespace VC {
         callback.OnCounterexample(newCounterexample, null);

       }

 

-      private Counterexample GenerateTrace(IList<string/*!*/>/*!*/ labels, ErrorModel/*!*/ errModel,

+      private Counterexample GenerateTrace(IList<string/*!*/>/*!*/ labels, ErrorModel/*!*/ errModel, ModelViewInfo mvInfo,

                                            int candidateId, Implementation procImpl) {

         Contract.Requires(errModel != null);

         Contract.Requires(cce.NonNullElements(labels));

@@ -3281,14 +3294,14 @@ namespace VC {
         trace.Add(entryBlock);

 

         var calleeCounterexamples = new Dictionary<TraceLocation, CalleeCounterexampleInfo>();

-        Counterexample newCounterexample = GenerateTraceRec(labels, errModel, candidateId, entryBlock, traceNodes, trace, calleeCounterexamples);

+        Counterexample newCounterexample = GenerateTraceRec(labels, errModel, mvInfo, candidateId, entryBlock, traceNodes, trace, calleeCounterexamples);

 

         return newCounterexample;

 

       }

 

       private Counterexample GenerateTraceRec(

-                            IList<string/*!*/>/*!*/ labels, ErrorModel/*!*/ errModel, int candidateId,

+                            IList<string/*!*/>/*!*/ labels, ErrorModel/*!*/ errModel, ModelViewInfo mvInfo, int candidateId,

                             Block/*!*/ b, Hashtable/*!*/ traceNodes, BlockSeq/*!*/ trace,

                             Dictionary<TraceLocation/*!*/, CalleeCounterexampleInfo/*!*/>/*!*/ calleeCounterexamples) {

         Contract.Requires(cce.NonNullElements(labels));

@@ -3309,7 +3322,7 @@ namespace VC {
                 // Skip if 'cmd' not contained in the trace or not an assert

                 if (cmd is AssertCmd && traceNodes.Contains(cmd))

                 {

-                    Counterexample newCounterexample = AssertCmdToCounterexample((AssertCmd)cmd, transferCmd, trace, errModel, new Dictionary<Incarnation, Absy/*!*/>());

+                    Counterexample newCounterexample = AssertCmdToCounterexample((AssertCmd)cmd, transferCmd, trace, errModel, mvInfo, new Dictionary<Incarnation, Absy/*!*/>());

                     newCounterexample.AddCalleeCounterexample(calleeCounterexamples);

                     return newCounterexample;

                 }

@@ -3331,7 +3344,7 @@ namespace VC {
 

                 calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] =

                     new CalleeCounterexampleInfo(

-                        cce.NonNull(GenerateTrace(labels, errModel, calleeId, implName2StratifiedInliningInfo[calleeName].impl)),

+                        cce.NonNull(GenerateTrace(labels, errModel, mvInfo, calleeId, implName2StratifiedInliningInfo[calleeName].impl)),

                         new List<object>());

 

             }

@@ -3602,7 +3615,7 @@ namespace VC {
       #endregion

     }

 

-    protected Hashtable/*TransferCmd->ReturnCmd*/ PassifyImpl(Implementation impl, Program program)

+    protected Hashtable/*TransferCmd->ReturnCmd*/ PassifyImpl(Implementation impl, Program program, out ModelViewInfo mvInfo)

     {

       Contract.Requires(impl != null);

       Contract.Requires(program != null);

@@ -3687,7 +3700,7 @@ namespace VC {
         Microsoft.Boogie.LiveVariableAnalysis.ComputeLiveVariables(impl);

       }

       

-      Hashtable exitIncarnationMap = Convert2PassiveCmd(impl);

+      Hashtable exitIncarnationMap = Convert2PassiveCmd(impl, out mvInfo);

 

       if (implName2LazyInliningInfo != null && implName2LazyInliningInfo.ContainsKey(impl.Name))

       {

@@ -3929,7 +3942,7 @@ namespace VC {
     }

 

     private static Counterexample LazyCounterexample(

-                                       ErrorModel/*!*/ errModel,

+                                       ErrorModel/*!*/ errModel, ModelViewInfo mvInfo,

                                        Dictionary<string/*!*/, LazyInliningInfo/*!*/>/*!*/ implName2LazyInliningInfo,

                                        ProverContext/*!*/ context,

                                        Program/*!*/ program,

@@ -3966,7 +3979,7 @@ namespace VC {
           if (assertCmd != null && errModel.LookupControlFlowFunctionAt(cfcValue, assertCmd.UniqueId) == 0)

           {

             Counterexample newCounterexample;

-            newCounterexample = AssertCmdToCounterexample(assertCmd, transferCmd, trace, errModel, cce.NonNull(info.incarnationOriginMap));

+            newCounterexample = AssertCmdToCounterexample(assertCmd, transferCmd, trace, errModel, mvInfo, cce.NonNull(info.incarnationOriginMap));

             newCounterexample.AddCalleeCounterexample(calleeCounterexamples);

             return newCounterexample;

           }

@@ -4047,7 +4060,7 @@ namespace VC {
           }

           calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] = 

             new CalleeCounterexampleInfo(

-              LazyCounterexample(errModel, implName2LazyInliningInfo, context, program, calleeName, args),

+              LazyCounterexample(errModel, mvInfo, implName2LazyInliningInfo, context, program, calleeName, args),

               errModel.PartitionsToValues(args));

         }

           

@@ -4071,7 +4084,7 @@ namespace VC {
     }

 

     static Counterexample TraceCounterexample(

-                          Block/*!*/ b, Hashtable/*!*/ traceNodes, BlockSeq/*!*/ trace, ErrorModel errModel,

+                          Block/*!*/ b, Hashtable/*!*/ traceNodes, BlockSeq/*!*/ trace, ErrorModel errModel, ModelViewInfo mvInfo,

                           Dictionary<Incarnation, Absy/*!*/>/*!*/ incarnationOriginMap,

                           Dictionary<string/*!*/, LazyInliningInfo/*!*/>/*!*/ implName2LazyInliningInfo,

                           ProverContext/*!*/ context, Program/*!*/ program,

@@ -4097,7 +4110,7 @@ namespace VC {
         // Skip if 'cmd' not contained in the trace or not an assert

         if (cmd is AssertCmd && traceNodes.Contains(cmd))

         {

-          Counterexample newCounterexample = AssertCmdToCounterexample((AssertCmd)cmd, transferCmd, trace, errModel, incarnationOriginMap);

+          Counterexample newCounterexample = AssertCmdToCounterexample((AssertCmd)cmd, transferCmd, trace, errModel, mvInfo, incarnationOriginMap);

           Contract.Assert(newCounterexample != null);

           newCounterexample.AddCalleeCounterexample(calleeCounterexamples);

           return newCounterexample;

@@ -4134,7 +4147,7 @@ namespace VC {
         }

         calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] = 

             new CalleeCounterexampleInfo(

-                LazyCounterexample(errModel, implName2LazyInliningInfo, context, program, calleeName, args),

+                LazyCounterexample(errModel, mvInfo, implName2LazyInliningInfo, context, program, calleeName, args),

                 errModel.PartitionsToValues(args));

         #endregion

       }

@@ -4147,7 +4160,7 @@ namespace VC {
           Contract.Assert(bb != null);

           if (traceNodes.Contains(bb)){

             trace.Add(bb);

-            return TraceCounterexample(bb, traceNodes, trace, errModel, incarnationOriginMap, implName2LazyInliningInfo, context, program, calleeCounterexamples);

+            return TraceCounterexample(bb, traceNodes, trace, errModel, mvInfo, incarnationOriginMap, implName2LazyInliningInfo, context, program, calleeCounterexamples);

           }

         }

       }

@@ -4646,7 +4659,7 @@ namespace VC {
       Dictionary<Bpl.Expr/*!*/, object>/*!*/ exprToPrintableValue) 

       //modifies exprToPrintableValue.*;

     {

-    Contract.Requires(expr != null);

+      Contract.Requires(expr != null);

       Contract.Requires(incarnationMap != null);

       Contract.Requires(errModel != null);

       Contract.Requires(exprToPrintableValue != null);

@@ -4863,17 +4876,16 @@ namespace VC {
       else {

         Contract.Assert(false);throw new cce.UnreachableException();  // unexpected Bpl.Expr

       }

-      return -1;

     }

 

-    static Counterexample AssertCmdToCounterexample(AssertCmd cmd, TransferCmd transferCmd, BlockSeq trace, ErrorModel errModel,

+    static Counterexample AssertCmdToCounterexample(AssertCmd cmd, TransferCmd transferCmd, BlockSeq trace, ErrorModel errModel, ModelViewInfo mvInfo,

       Dictionary<Incarnation, Absy> incarnationOriginMap) 

-  {

-    Contract.Requires(cmd != null);

-    Contract.Requires(transferCmd != null);

-    Contract.Requires(trace != null);

+    {

+      Contract.Requires(cmd != null);

+      Contract.Requires(transferCmd != null);

+      Contract.Requires(trace != null);

       Contract.Requires(cce.NonNullElements(incarnationOriginMap));

-    Contract.Ensures(Contract.Result<Counterexample>() != null);

+      Contract.Ensures(Contract.Result<Counterexample>() != null);

 

       List<string> relatedInformation = new List<string>();

       if (CommandLineOptions.Clo.EnhancedErrorMessages == 1) {

@@ -4892,7 +4904,7 @@ namespace VC {
       {

         AssertRequiresCmd assertCmd = (AssertRequiresCmd)cmd;

         Contract.Assert(assertCmd != null);

-        CallCounterexample cc = new CallCounterexample(trace, assertCmd.Call, assertCmd.Requires);

+        CallCounterexample cc = new CallCounterexample(trace, assertCmd.Call, assertCmd.Requires, errModel, mvInfo);

         cc.relatedInformation = relatedInformation;

         return cc;

       }

@@ -4900,13 +4912,13 @@ namespace VC {
       {

         AssertEnsuresCmd assertCmd = (AssertEnsuresCmd)cmd;

         Contract.Assert(assertCmd != null);

-        ReturnCounterexample rc = new ReturnCounterexample(trace, transferCmd, assertCmd.Ensures);

+        ReturnCounterexample rc = new ReturnCounterexample(trace, transferCmd, assertCmd.Ensures, errModel, mvInfo);

         rc.relatedInformation = relatedInformation;

         return rc;

       }

       else 

       {

-        AssertCounterexample ac = new AssertCounterexample(trace, (AssertCmd)cmd);

+        AssertCounterexample ac = new AssertCounterexample(trace, (AssertCmd)cmd, errModel, mvInfo);

         ac.relatedInformation = relatedInformation;

         return ac;

       }

diff --git a/Source/VCGeneration/VCDoomed.cs b/Source/VCGeneration/VCDoomed.cs
index c1547009..d97ee0fd 100644
--- a/Source/VCGeneration/VCDoomed.cs
+++ b/Source/VCGeneration/VCDoomed.cs
@@ -302,8 +302,6 @@ namespace VC {
       watch.Reset();

       watch.Start();

 

-

-

       #region Transform the Program into loop-free passive form

       variable2SequenceNumber = new Hashtable/*Variable -> int*/();

       incarnationOriginMap = new Dictionary<Incarnation, Absy>();

@@ -329,7 +327,8 @@ namespace VC {
       if (UseItAsDebugger)

         RemoveReachVars(cce.NonNull(firstDebugBlock));

 

-      PassifyProgram(impl);

+      ModelViewInfo mvInfo;

+      PassifyProgram(impl, out mvInfo);

 

       #endregion

       //EmitImpl(impl,false);

@@ -737,8 +736,6 @@ namespace VC {
         b.Cmds = backup;

         return false;

       }

-

-      return false;

     }

 

     void UndoBlockModifications(Implementation impl, Dictionary<Block/*!*/, CmdSeq/*!*/>/*!*/ cmdbackup,

@@ -1079,8 +1076,6 @@ namespace VC {
         Contract.Requires(cutPoint != null);

         Contract.Requires(cce.NonNullElements(loopNodes));

         loopNodes.Add(current);

-        if (false)

-          System.Diagnostics.Debugger.Break();

         foreach (GraphNode g in current.Predecessors) {

           Contract.Assert(g != null);

           if (cutPoint.firstPredecessor == g || g == cutPoint || loopNodes.Contains(g))

@@ -1318,12 +1313,12 @@ namespace VC {
     }

 

 

-    private Hashtable/*TransferCmd->ReturnCmd*/ PassifyProgram(Implementation impl) {

+    private Hashtable/*TransferCmd->ReturnCmd*/ PassifyProgram(Implementation impl, out ModelViewInfo mvInfo) {

       Contract.Requires(impl != null);

       Contract.Ensures(Contract.Result<Hashtable>() != null);

 

       CurrentLocalVariables = impl.LocVars;

-      Convert2PassiveCmd(impl);

+      Convert2PassiveCmd(impl, out mvInfo);

       return new Hashtable();

     }

 

diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index d29223a9..1c67e06b 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -68,13 +68,16 @@ namespace VC {
       }

       

       int id = b.UniqueId;

-      cce.BeginExpose(ctxt); {

+      try {

+        cce.BeginExpose(ctxt);

         ctxt.Label2absy[id] = b;

         if (ctxt.ControlFlowVariable != null)

           return res;

-        else 

+        else

           return gen.Implies(gen.LabelPos(cce.NonNull(id.ToString()), VCExpressionGenerator.True), res);

-      }cce.EndExpose();

+      } finally {

+        cce.EndExpose();

+      }

     }

 

     /// <summary>

@@ -112,7 +115,7 @@ namespace VC {
               Contract.Assert(false);throw new cce.UnreachableException();  // unexpected case

           }

           

-          // (MSchaef) Hack: This line might be useless, but at least it is not harmfull

+          // (MSchaef) Hack: This line might be useless, but at least it is not harmful

           // need to test it

           if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) 

             return gen.Implies(C, N);

diff --git a/Test/test15/Answer b/Test/test15/Answer
index 8452acb6..969bbe41 100644
--- a/Test/test15/Answer
+++ b/Test/test15/Answer
@@ -55,7 +55,7 @@ False : *1
 End of model.

 NullInModel.bpl(2,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        NullInModel.bpl(2,3): anon0

+    NullInModel.bpl(2,3): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

 

@@ -104,7 +104,7 @@ False : *1
 End of model.

 IntInModel.bpl(2,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        IntInModel.bpl(2,3): anon0

+    IntInModel.bpl(2,3): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

 

@@ -174,19 +174,34 @@ False : *1
 End of model.

 ModelTest.bpl(7,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        ModelTest.bpl(3,5): anon0

+    ModelTest.bpl(3,5): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

 

 -------------------- InterpretedFunctionTests --------------------

 InterpretedFunctionTests.bpl(4,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        InterpretedFunctionTests.bpl(2,3): anon0

+    InterpretedFunctionTests.bpl(2,3): anon0

 InterpretedFunctionTests.bpl(10,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        InterpretedFunctionTests.bpl(8,3): anon0

+    InterpretedFunctionTests.bpl(8,3): anon0

 InterpretedFunctionTests.bpl(16,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        InterpretedFunctionTests.bpl(14,3): anon0

+    InterpretedFunctionTests.bpl(14,3): anon0

 

 Boogie program verifier finished with 0 verified, 3 errors

+

+-------------------- CaptureState --------------------

+CaptureState.bpl(26,1): Error BP5003: A postcondition might not hold on this return path.

+CaptureState.bpl(8,3): Related location: This is the postcondition that might not hold.

+Execution trace:

+    CaptureState.bpl(12,3): anon0

+    CaptureState.bpl(16,5): anon4_Then

+    CaptureState.bpl(24,5): anon3

+Captured states:

+    top

+    then

+    postUpdate0

+    end

+

+Boogie program verifier finished with 0 verified, 1 error

diff --git a/Test/test15/CaptureState.bpl b/Test/test15/CaptureState.bpl
new file mode 100644
index 00000000..7c73c411
--- /dev/null
+++ b/Test/test15/CaptureState.bpl
@@ -0,0 +1,26 @@
+type Ref;

+type FieldName;

+var Heap: [Ref,FieldName]int;

+

+const unique F: FieldName;

+

+procedure P(this: Ref, x: int, y: int) returns (r: int)

+  ensures 0 <= r;

+{

+  var m: int;

+

+  assume {:captureState "top"} true;

+

+  m := Heap[this, F];

+  if (0 <= x) {

+    assume {:captureState "then"} true;

+    m := m + 1;

+    assume {:captureState "postUpdate0"} true;

+  } else {

+    assume {:captureState "else"} true;

+    m := (m + y) * (m + y);

+    assume {:captureState "postUpdate1"} true;

+  }

+  r := m + m;

+  assume {:captureState "end"} true;

+}

diff --git a/Test/test15/runtest.bat b/Test/test15/runtest.bat
index 90771065..fc25c876 100644
--- a/Test/test15/runtest.bat
+++ b/Test/test15/runtest.bat
@@ -9,8 +9,8 @@ for %%f in (NullInModel IntInModel ModelTest) do (
   echo -------------------- %%f --------------------

   "%BGEXE%" %* %%f.bpl /printModel:2

 )

-for %%f in (InterpretedFunctionTests) do (

+for %%f in (InterpretedFunctionTests CaptureState) do (

   echo.

   echo -------------------- %%f --------------------

-  "%BGEXE%" %* %%f.bpl 

+  "%BGEXE%" %* %%f.bpl

 )