various cleanup regarding /doNotUseLabels

1 files changed, 8 insertions, 17 deletions

diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs
index c12c6d8b..a2bf0304 100644
--- a/Source/Houdini/Checker.cs
+++ b/Source/Houdini/Checker.cs
@@ -22,8 +22,6 @@ namespace Microsoft.Boogie.Houdini {
     private VCExpr conjecture;

     private ProverInterface.ErrorHandler handler;

     ConditionGeneration.CounterexampleCollector collector;

-    LocalVariable controlFlowVariable;

-    int entryBlockId;

 

     public HoudiniSession(VCGen vcgen, Checker checker, Program program, Implementation impl) {

       descriptiveName = impl.Name;

@@ -35,13 +33,16 @@ namespace Microsoft.Boogie.Houdini {
       Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = vcgen.PassifyImpl(impl, program, out mvInfo);

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

 

+      var exprGen = checker.TheoremProver.Context.ExprGen;

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

+      

+      conjecture = vcgen.GenerateVC(impl, controlFlowVariableExpr, out label2absy, checker);

+

       if (!CommandLineOptions.Clo.UseLabels) {

-        controlFlowVariable = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "@cfc", Microsoft.Boogie.Type.Int));

-        impl.LocVars.Add(controlFlowVariable);

-        entryBlockId = impl.Blocks[0].UniqueId;

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

+        conjecture = exprGen.Implies(eqExpr, conjecture);

       }

-      

-      conjecture = vcgen.GenerateVC(impl, controlFlowVariable, out label2absy, checker);

 

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

         handler = new VCGen.ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, vcgen.incarnationOriginMap, collector, mvInfo, vcgen.implName2LazyInliningInfo, checker.TheoremProver.Context, program);

@@ -55,16 +56,6 @@ namespace Microsoft.Boogie.Houdini {
       collector.examples.Clear();

       VCExpr vc = checker.VCExprGen.Implies(axiom, conjecture);

 

-      if (!CommandLineOptions.Clo.UseLabels) {

-        var ctx = checker.TheoremProver.Context;

-        var bet = ctx.BoogieExprTranslator;

-        VCExpr controlFlowVariableExpr = bet.LookupVariable(controlFlowVariable);

-        VCExpr eqExpr1 = ctx.ExprGen.Eq(controlFlowVariableExpr, ctx.ExprGen.Integer(BigNum.ZERO));

-        VCExpr controlFlowFunctionAppl = ctx.ExprGen.ControlFlowFunctionApplication(controlFlowVariableExpr, ctx.ExprGen.Integer(BigNum.ZERO));

-        VCExpr eqExpr2 = ctx.ExprGen.Eq(controlFlowFunctionAppl, ctx.ExprGen.Integer(BigNum.FromInt(entryBlockId)));

-        vc = ctx.ExprGen.Implies(eqExpr1, ctx.ExprGen.Implies(eqExpr2, vc));

-      }

-

       DateTime now = DateTime.UtcNow;

       checker.BeginCheck(descriptiveName, vc, handler);

       WaitHandle.WaitAny(new WaitHandle[] { checker.ProverDone });