Merge

1 files changed, 11 insertions, 22 deletions

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 34c12549..22330b3e 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -31,6 +31,7 @@ namespace VC
         private bool useSummary;

         private SummaryComputation summaryComputation;

         private HashSet<string> procsThatReachedRecBound;

+        public int boundUsedInLastQuery { get; private set; }

         ProverInterface prover;

         public HashSet<string> procsToSkip;

         public Dictionary<string, int> extraRecBound;

@@ -62,7 +63,7 @@ namespace VC
             procsThatReachedRecBound = new HashSet<string>();

             procsToSkip = new HashSet<string>();

             extraRecBound = new Dictionary<string, int>();

-            //extraRecBound.Add("FcFinishReset_loop_label_59_head", 4);

+            boundUsedInLastQuery = -1;

         }

 

         // Is this procedure to be "skipped" 

@@ -295,7 +296,7 @@ namespace VC
           public Hashtable/*<int, Absy!>*/ label2absy;

           public ModelViewInfo mvInfo;

           public Dictionary<Block, List<CallSite>> callSites;

-          public bool initialized;

+          public bool initialized { get; private set; }

 

           public StratifiedInliningInfo(Implementation implementation, StratifiedVCGen stratifiedVcGen) {

             vcgen = stratifiedVcGen;

@@ -344,7 +345,8 @@ namespace VC
             initialized = false;

           }

 

-          public void GenerateVC() {

+          public void GenerateVC()  {

+            if (initialized) return;

             List<Variable> outputVariables = new List<Variable>();

             assertExpr = new LiteralExpr(Token.NoToken, true);

             foreach (Variable v in impl.OutParams) {

@@ -1133,27 +1135,12 @@ namespace VC
             Contract.Assert(implName2StratifiedInliningInfo != null);

 

             // Build VCs for all procedures

-            foreach (StratifiedInliningInfo info in implName2StratifiedInliningInfo.Values)

-            {

-                Contract.Assert(info != null);

-                info.GenerateVC();

-            }

+            implName2StratifiedInliningInfo.Values

+                .Iter(info => info.GenerateVC());

 

             // Get the VC of the current procedure

-            VCExpr vcMain;

-            Hashtable/*<int, Absy!>*/ mainLabel2absy;

-            ModelViewInfo mvInfo;

-

-            ConvertCFG2DAG(impl);

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

-            var exprGen = prover.Context.ExprGen;

-            VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO); 

-            vcMain = GenerateVC(impl, controlFlowVariableExpr, out mainLabel2absy, prover.Context);

-            if (!CommandLineOptions.Clo.UseLabels) {

-              VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(exprGen.Integer(BigNum.ZERO), exprGen.Integer(BigNum.ZERO));

-              VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId)));

-              vcMain = exprGen.Implies(eqExpr, vcMain);

-            }

+            VCExpr vcMain = implName2StratifiedInliningInfo[impl.Name].vcexpr;

+            Hashtable/*<int, Absy!>*/ mainLabel2absy = implName2StratifiedInliningInfo[impl.Name].label2absy;

 

             // Find all procedure calls in vc and put labels on them      

             FCallHandler calls = new FCallHandler(prover.VCExprGen, implName2StratifiedInliningInfo, impl.Name, mainLabel2absy);

@@ -1520,6 +1507,8 @@ namespace VC
             //   case 3: (internal error)   The theorem prover TimesOut of runs OutOfMemory

             while (true)

             {

+                boundUsedInLastQuery = bound;

+

                 // Check timeout

                 if (CommandLineOptions.Clo.ProverKillTime != -1)

                 {