Boogie:

* Added Test/textbook/DivMod.bpl, which embodies a conversion between C's div/mod operators and SMT Lib's div/mod operators.
* Added a rudimentary printing of variables for captured states.  It doesn't attempt to print everything at this time, and it doesn't work when variables get unique-ified by @@-suffixes.  A more complete implementation will be added at a later time.

1 files changed, 4 insertions, 4 deletions

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

             vcgen.ComputePredecessors(codeExpr.Blocks);

             vcgen.AddBlocksBetween(codeExpr.Blocks);

-            ModelViewInfo mvInfoCodeExpr;

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

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

             VCExpr startCorrect = VCGen.LetVC(

 		      codeExpr.Blocks[0],

               null,

@@ -3699,8 +3698,9 @@ namespace VC {
       if (CommandLineOptions.Clo.LiveVariableAnalysis > 0) {

         Microsoft.Boogie.LiveVariableAnalysis.ComputeLiveVariables(impl);

       }

-      

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

+

+      mvInfo = new ModelViewInfo(program, impl);

+      Hashtable exitIncarnationMap = Convert2PassiveCmd(impl, mvInfo);

 

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

       {