From 073ddcc74e239cb9b270cc2e6db60e1daa033518 Mon Sep 17 00:00:00 2001 From: "U-REDMOND\\kenmcmil" Date: Tue, 9 Jun 2015 15:51:05 -0700 Subject: various changes for duality from dead codeplex repo --- Source/VCGeneration/Check.cs | 3 +- Source/VCGeneration/FixedpointVC.cs | 56 ++++++++++++++++++++++--------------- 2 files changed, 35 insertions(+), 24 deletions(-) (limited to 'Source/VCGeneration') diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index 33baf798..71ae21c6 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -449,7 +449,8 @@ namespace Microsoft.Boogie { Invalid, TimeOut, OutOfMemory, - Undetermined + Undetermined, + Bounded } public class ErrorHandler { // Used in CheckOutcomeCore diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs index 5c698633..70ce5a8f 100644 --- a/Source/VCGeneration/FixedpointVC.cs +++ b/Source/VCGeneration/FixedpointVC.cs @@ -480,13 +480,6 @@ namespace Microsoft.Boogie List interfaceVars = new List(); Expr assertExpr = new LiteralExpr(Token.NoToken, true); Contract.Assert(assertExpr != null); - foreach (Variable v in program.GlobalVariables) - { - Contract.Assert(v != null); - interfaceVars.Add(v); - if (v.Name == "error") - inputErrorVariable = v; - } // InParams must be obtained from impl and not proc foreach (Variable v in impl.InParams) { @@ -503,6 +496,13 @@ namespace Microsoft.Boogie Expr eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, c), new IdentifierExpr(Token.NoToken, v)); assertExpr = Expr.And(assertExpr, eqExpr); } + foreach (Variable v in program.GlobalVariables) + { + Contract.Assert(v != null); + interfaceVars.Add(v); + if (v.Name == "error") + inputErrorVariable = v; + } if (errorVariable != null) { proc.Modifies.Add(new IdentifierExpr(Token.NoToken, errorVariable)); @@ -657,11 +657,6 @@ namespace Microsoft.Boogie } else if (mode == Mode.Corral || proc.FindExprAttribute("inline") != null || proc is LoopProcedure) { - foreach (Variable v in program.GlobalVariables) - { - Contract.Assert(v != null); - exprs.Add(new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v))); - } foreach (Variable v in proc.InParams) { Contract.Assert(v != null); @@ -672,6 +667,11 @@ namespace Microsoft.Boogie Contract.Assert(v != null); exprs.Add(new IdentifierExpr(Token.NoToken, v)); } + foreach (Variable v in program.GlobalVariables) + { + Contract.Assert(v != null); + exprs.Add(new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v))); + } foreach (IdentifierExpr ie in proc.Modifies) { Contract.Assert(ie != null); @@ -1513,7 +1513,7 @@ namespace Microsoft.Boogie /** Check the RPFP, and return a counterexample if there is one. */ - public RPFP.LBool Check(ref RPFP.Node cexroot) + public VC.ConditionGeneration.Outcome Check(ref RPFP.Node cexroot) { var start = DateTime.Now; @@ -1548,11 +1548,15 @@ namespace Microsoft.Boogie switch(outcome) { case ProverInterface.Outcome.Valid: - return RPFP.LBool.False; + return VC.ConditionGeneration.Outcome.Correct; + case ProverInterface.Outcome.Bounded: + return VC.ConditionGeneration.Outcome.ReachedBound; case ProverInterface.Outcome.Invalid: - return RPFP.LBool.True; + return VC.ConditionGeneration.Outcome.Errors; + case ProverInterface.Outcome.TimeOut: + return VC.ConditionGeneration.Outcome.TimedOut; default: - return RPFP.LBool.Undef; + return VC.ConditionGeneration.Outcome.Inconclusive; } } @@ -1598,7 +1602,7 @@ namespace Microsoft.Boogie Console.WriteLine("check: {0}s", (DateTime.Now - start).TotalSeconds); switch (checkres) { - case RPFP.LBool.True: + case Outcome.Errors: Console.WriteLine("Counterexample found.\n"); // start = DateTime.Now; Counterexample cex = CreateBoogieCounterExample(cexroot.owner, cexroot, impl); @@ -1607,17 +1611,23 @@ namespace Microsoft.Boogie collector.OnCounterexample(cex, "assertion failure"); Console.WriteLine("cex: {0}s", (DateTime.Now - start).TotalSeconds); ConjecturesToSpecs(); - return VC.ConditionGeneration.Outcome.Errors; - case RPFP.LBool.False: - Console.WriteLine("Procedure is correct."); + break; + case Outcome.Correct: + Console.WriteLine("Procedure is correct. (fixed point reached)"); FixedPointToSpecs(); ConjecturesToSpecs(); - return Outcome.Correct; - case RPFP.LBool.Undef: + break; + case Outcome.ReachedBound: + Console.WriteLine("Procedure is correct. (recursion bound reached)"); + FixedPointToSpecs(); + ConjecturesToSpecs(); + break; + default: Console.WriteLine("Inconclusive result."); ConjecturesToSpecs(); - return Outcome.ReachedBound; + break; } + return checkres; } -- cgit v1.2.3