diff options
author | 2013-09-04 20:48:01 -0700 | |
---|---|---|
committer | 2013-09-04 20:48:01 -0700 | |
commit | 750b3b36959588e2a063a5246c04104d2ebea9a7 (patch) | |
tree | a2972a7dd99cf0ab1fa08d7b0ef66dde1d49ddff /Source/VCGeneration | |
parent | 928b0875faa34b0d9d9162dbbb6e5fadf7044aac (diff) |
When a codeexpr is used at the top-level in an assume statement, we use the alternative existential semantics.
Diffstat (limited to 'Source/VCGeneration')
-rw-r--r-- | Source/VCGeneration/VC.cs | 26 | ||||
-rw-r--r-- | Source/VCGeneration/Wlp.cs | 13 |
2 files changed, 32 insertions, 7 deletions
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 3b8bb054..7cd9f9c2 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1345,7 +1345,7 @@ namespace VC { this.ctx = ctx;
}
- public VCExpr CodeExprToVerificationCondition(CodeExpr codeExpr, Hashtable blockVariables, List<VCExprLetBinding> bindings)
+ public VCExpr CodeExprToVerificationCondition(CodeExpr codeExpr, Hashtable blockVariables, List<VCExprLetBinding> bindings, bool isAssumeContext)
{
VCGen vcgen = new VCGen(new Program(), null, false, new List<Checker>());
vcgen.variable2SequenceNumber = new Dictionary<Variable, int>();
@@ -1356,9 +1356,12 @@ namespace VC { vcgen.AddBlocksBetween(codeExpr.Blocks);
Dictionary<Variable, Expr> gotoCmdOrigins = vcgen.ConvertBlocks2PassiveCmd(codeExpr.Blocks, new List<IdentifierExpr>(), new ModelViewInfo(codeExpr));
int ac; // computed, but then ignored for this CodeExpr
- VCExpr startCorrect = VCGen.LetVC(codeExpr.Blocks[0], null, label2absy, blockVariables, bindings, ctx, out ac);
+ VCExpr startCorrect = VCGen.LetVCIterative(codeExpr.Blocks, null, label2absy, ctx, out ac, isAssumeContext);
VCExpr vce = ctx.ExprGen.Let(bindings, startCorrect);
-
+ if (isAssumeContext)
+ {
+ vce = ctx.ExprGen.Not(vce);
+ }
if (vcgen.CurrentLocalVariables.Count != 0)
{
Boogie2VCExprTranslator translator = ctx.BoogieExprTranslator;
@@ -1375,7 +1378,14 @@ namespace VC { vce = ctx.ExprGen.Implies(ctx.ExprGen.Function(VCExpressionGenerator.TickleBoolOp, ev), vce);
}
}
- vce = ctx.ExprGen.Forall(boundVars, new List<VCTrigger>(), vce);
+ if (isAssumeContext)
+ {
+ vce = ctx.ExprGen.Exists(boundVars, new List<VCTrigger>(), vce);
+ }
+ else
+ {
+ vce = ctx.ExprGen.Forall(boundVars, new List<VCTrigger>(), vce);
+ }
}
return vce;
}
@@ -2706,7 +2716,9 @@ namespace VC { VCExpr controlFlowVariableExpr,
Dictionary<int, Absy> label2absy,
ProverContext proverCtxt,
- out int assertionCount) {
+ out int assertionCount,
+ bool isAssumeContext = false)
+ {
Contract.Requires(blocks != null);
Contract.Requires(proverCtxt != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
@@ -2743,6 +2755,10 @@ namespace VC { else {
SuccCorrect = proverCtxt.BoogieExprTranslator.Translate(re.Expr);
}
+ if (isAssumeContext)
+ {
+ SuccCorrect = gen.Not(SuccCorrect);
+ }
}
else {
Contract.Assert(gotocmd.labelTargets != null);
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index 277d9a94..b1e69c38 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -160,8 +160,17 @@ namespace VC { }
}
- return gen.ImpliesSimp(ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr), N);
-
+ CodeExpr codeExpr = ac.Expr as CodeExpr;
+ if (codeExpr != null)
+ {
+ Hashtable blockVariables = new Hashtable();
+ List<VCExprLetBinding> bindings = new List<VCExprLetBinding>();
+ return gen.ImpliesSimp(ctxt.Ctxt.BoogieExprTranslator.codeExprConverter(codeExpr, blockVariables, bindings, true), N);
+ }
+ else
+ {
+ return gen.ImpliesSimp(ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr), N);
+ }
} else {
Console.WriteLine(cmd.ToString());
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected command
|