diff options
| author |  Unknown <qadeer@Shakespeare.redmond.corp.microsoft.com> | 2011-04-14 22:34:06 -0700 |
|---|---|---|
| committer | Unknown <qadeer@Shakespeare.redmond.corp.microsoft.com> | 2011-04-14 22:34:06 -0700 |
| commit | 6e683025dbc6b7b6f74ed9415178f6f4abff2a24 (patch) | |
| tree | f4eb2a9add18fe78600f6d3a32f3d20c6067ebb4 /Source/VCGeneration/Wlp.cs | |
| parent | ddd16cd53910f044fd4700463ff977091b983897 (diff) | |
added reachability information to the VC and used that to support arbitrary asserts in lazy inlining
Diffstat (limited to 'Source/VCGeneration/Wlp.cs')
| -rw-r--r-- | Source/VCGeneration/Wlp.cs | 19 |
1 files changed, 7 insertions, 12 deletions
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index 1c67e06b..0b2c3225 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -64,7 +64,7 @@ namespace VC { for (int i = b.Cmds.Length; --i >= 0; )
{
- res = Cmd(cce.NonNull( b.Cmds[i]), res, ctxt);
+ res = Cmd(b, cce.NonNull( b.Cmds[i]), res, ctxt);
}
int id = b.UniqueId;
@@ -83,7 +83,7 @@ namespace VC { /// <summary>
/// Computes the wlp for an assert or assume command "cmd".
/// </summary>
- public static VCExpr Cmd(Cmd cmd, VCExpr N, VCContext ctxt)
+ public static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt)
{
Contract.Requires(cmd!= null);
Contract.Requires(N != null);
@@ -122,17 +122,12 @@ namespace VC { if (ctxt.ControlFlowVariable != null)
{
- VCExpr controlFlowVariableExpr =
- ctxt.Ctxt.BoogieExprTranslator.LookupVariable(ctxt.ControlFlowVariable);
+ VCExpr controlFlowVariableExpr = ctxt.Ctxt.BoogieExprTranslator.LookupVariable(ctxt.ControlFlowVariable);
Contract.Assert(controlFlowVariableExpr != null);
- VCExpr controlFlowFunctionAppl1 =
- gen.ControlFlowFunctionApplication(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(id)));
- Contract.Assert(controlFlowFunctionAppl1 != null);
- VCExpr controlFlowFunctionAppl2 =
- gen.ControlFlowFunctionApplication(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(id)));
- VCExpr assertFailure = gen.Eq(controlFlowFunctionAppl1, gen.Integer(BigNum.FromInt(0)));
- VCExpr assertSuccess = gen.Neq(controlFlowFunctionAppl2, gen.Integer(BigNum.FromInt(0)));
- return gen.And(gen.Implies(assertFailure, C), gen.Implies(assertSuccess, N));
+ VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(b.UniqueId)));
+ Contract.Assert(controlFlowFunctionAppl != null);
+ VCExpr assertFailure = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(ac.UniqueId)));
+ return gen.And(gen.Implies(assertFailure, C), gen.Implies(C, N));
}
else
return gen.AndSimp(gen.LabelNeg(cce.NonNull(id.ToString()), C), N);
|