diff options
author | 2012-02-25 14:01:25 -0800 | |
---|---|---|
committer | 2012-02-25 14:01:25 -0800 | |
commit | 88679e1cc6fb26590886686519987fa958a2735b (patch) | |
tree | b4eeb488c474724d01cf949091b19427c5c1b859 /Source/VCGeneration/VC.cs | |
parent | 44cc8ee3486a320aae809bc4755f4da8c4de4b79 (diff) |
further fixes related to using uninterpreted function for error traces
removed Provers.Simplify, Provers.Z3, Provers.TPTP from the solution
Diffstat (limited to 'Source/VCGeneration/VC.cs')
-rw-r--r-- | Source/VCGeneration/VC.cs | 44 |
1 files changed, 36 insertions, 8 deletions
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 49fa7144..1c0aeee8 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -607,8 +607,30 @@ namespace VC { Hashtable label2Absy;
Checker ch = parent.FindCheckerFor(impl, CommandLineOptions.Clo.SmokeTimeout);
Contract.Assert(ch != null);
- VCExpr vc = parent.GenerateVC(impl, null, out label2Absy, ch);
+
+ Variable controlFlowVariable = null;
+ if (!CommandLineOptions.Clo.UseLabels) {
+ foreach (Variable v in impl.LocVars) {
+ if (v.Name == "@cfc") {
+ controlFlowVariable = v;
+ break;
+ }
+ }
+ }
+
+ VCExpr vc = parent.GenerateVC(impl, controlFlowVariable, out label2Absy, ch);
Contract.Assert(vc != null);
+
+ if (!CommandLineOptions.Clo.UseLabels) {
+ var ctx = ch.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(impl.Blocks[0].UniqueId)));
+ vc = ctx.ExprGen.Implies(eqExpr1, ctx.ExprGen.Implies(eqExpr2, vc));
+ }
+
impl.Blocks = backup;
if (CommandLineOptions.Clo.TraceVerify) {
@@ -1537,7 +1559,6 @@ namespace VC { ));
LocalVariable controlFlowVariable = null;
-
if (!CommandLineOptions.Clo.UseLabels) {
controlFlowVariable = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "@cfc", Microsoft.Boogie.Type.Int));
impl.LocVars.Add(controlFlowVariable);
@@ -1548,10 +1569,10 @@ namespace VC { if (!CommandLineOptions.Clo.UseLabels) {
VCExpr controlFlowVariableExpr = bet.LookupVariable(controlFlowVariable);
- Contract.Assert(controlFlowVariableExpr != null);
+ VCExpr eqExpr1 = ctx.ExprGen.Eq(controlFlowVariableExpr, ctx.ExprGen.Integer(BigNum.ZERO));
VCExpr controlFlowFunctionAppl = ctx.ExprGen.ControlFlowFunctionApplication(controlFlowVariableExpr, ctx.ExprGen.Integer(BigNum.ZERO));
- Contract.Assert(controlFlowFunctionAppl != null);
- vc = ctx.ExprGen.Implies(ctx.ExprGen.Eq(controlFlowFunctionAppl, ctx.ExprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId))), vc);
+ VCExpr eqExpr2 = ctx.ExprGen.Eq(controlFlowFunctionAppl, ctx.ExprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId)));
+ vc = ctx.ExprGen.Implies(eqExpr1, ctx.ExprGen.Implies(eqExpr2, vc));
}
if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) {
@@ -1667,7 +1688,7 @@ namespace VC { break;
case CommandLineOptions.VCVariety.Dag:
if (cce.NonNull(CommandLineOptions.Clo.TheProverFactory).SupportsDags) {
- vc = DagVC(cce.NonNull(impl.Blocks[0]), label2absy, new Hashtable/*<Block, VCExpr!>*/(), ch.TheoremProver.Context, out assertionCount);
+ vc = DagVC(cce.NonNull(impl.Blocks[0]), controlFlowVariable, label2absy, new Hashtable/*<Block, VCExpr!>*/(), ch.TheoremProver.Context, out assertionCount);
} else {
vc = LetVC(cce.NonNull(impl.Blocks[0]), controlFlowVariable, label2absy, ch.TheoremProver.Context, out assertionCount);
}
@@ -3593,6 +3614,7 @@ namespace VC { }
static VCExpr DagVC(Block block,
+ Variable controlFlowVariable,
Hashtable/*<int, Absy!>*/ label2absy,
Hashtable/*<Block, VCExpr!>*/ blockEquations,
ProverContext proverCtxt,
@@ -3623,8 +3645,14 @@ namespace VC { foreach (Block successor in cce.NonNull(gotocmd.labelTargets)) {
Contract.Assert(successor != null);
int ac;
- VCExpr c = DagVC(successor, label2absy, blockEquations, proverCtxt, out ac);
+ VCExpr c = DagVC(successor, controlFlowVariable, label2absy, blockEquations, proverCtxt, out ac);
assertionCount += ac;
+ if (controlFlowVariable != null) {
+ VCExprVar controlFlowVariableExpr = proverCtxt.BoogieExprTranslator.LookupVariable(controlFlowVariable);
+ VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(block.UniqueId)));
+ VCExpr controlTransferExpr = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(successor.UniqueId)));
+ c = gen.Implies(controlTransferExpr, c);
+ }
SuccCorrect = SuccCorrect == null ? c : gen.And(SuccCorrect, c);
}
}
@@ -3632,7 +3660,7 @@ namespace VC { SuccCorrect = VCExpressionGenerator.True;
}
- VCContext context = new VCContext(label2absy, proverCtxt);
+ VCContext context = new VCContext(label2absy, proverCtxt, controlFlowVariable);
vc = Wlp.Block(block, SuccCorrect, context);
assertionCount += context.AssertionCount;
|