diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/VCExpr/Boogie2VCExpr.cs | 6 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 26 | ||||
| -rw-r--r-- | Source/VCGeneration/Wlp.cs | 13 |
3 files changed, 35 insertions, 10 deletions
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index 0b92b1c3..e4101d49 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -47,7 +47,7 @@ namespace Microsoft.Boogie.VCExprAST { }
}
- public delegate VCExpr/*!*/ CodeExprConverter(CodeExpr/*!*/ codeExpr, Hashtable/*<Block, VCExprVar!>*//*!*/ blockVariables, List<VCExprLetBinding> bindings);
+ public delegate VCExpr/*!*/ CodeExprConverter(CodeExpr/*!*/ codeExpr, Hashtable/*<Block, VCExprVar!>*//*!*/ blockVariables, List<VCExprLetBinding> bindings, bool isAssumeContext);
public class Boogie2VCExprTranslator : StandardVisitor, ICloneable {
// Stack on which the various Visit-methods put the result of the translation
@@ -611,7 +611,7 @@ namespace Microsoft.Boogie.VCExprAST { Contract.Assert(false);
throw new cce.UnreachableException();
}
- CodeExprConverter codeExprConverter = null;
+ public CodeExprConverter codeExprConverter = null;
public void SetCodeExprConverter(CodeExprConverter f) {
this.codeExprConverter = f;
}
@@ -623,7 +623,7 @@ namespace Microsoft.Boogie.VCExprAST { Hashtable/*<Block, LetVariable!>*/ blockVariables = new Hashtable/*<Block, LetVariable!!>*/();
List<VCExprLetBinding/*!*/> bindings = new List<VCExprLetBinding/*!*/>();
- VCExpr e = codeExprConverter(codeExpr, blockVariables, bindings);
+ VCExpr e = codeExprConverter(codeExpr, blockVariables, bindings, false);
Push(e);
return codeExpr;
}
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
|