diff options
| author |  qadeer <qadeer@microsoft.com> | 2011-04-15 14:21:33 -0700 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2011-04-15 14:21:33 -0700 |
| commit | bf6fbc51ecf3d036efafec80d6852d1d01d161d4 (patch) | |
| tree | 6229da0051a5d9c27a7015c940c2526b6201547c /Source/VCGeneration/Wlp.cs | |
| parent | d034da855be7802a9a0e2157e3b5346dcb5f46b7 (diff) | |
modified letvc generation so that the use of control flow function and labels is decoupled. Former is controled by controlFlowVariable and the latter by label2Absy.
Diffstat (limited to 'Source/VCGeneration/Wlp.cs')
| -rw-r--r-- | Source/VCGeneration/Wlp.cs | 43 |
1 files changed, 29 insertions, 14 deletions
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index 0b2c3225..23be6082 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -68,13 +68,18 @@ namespace VC { }
int id = b.UniqueId;
+ if (ctxt.Label2absy != null) {
+ ctxt.Label2absy[id] = b;
+ }
+
try {
cce.BeginExpose(ctxt);
- ctxt.Label2absy[id] = b;
- if (ctxt.ControlFlowVariable != null)
+ if (ctxt.Label2absy == null) {
return res;
- else
+ }
+ else {
return gen.Implies(gen.LabelPos(cce.NonNull(id.ToString()), VCExpressionGenerator.True), res);
+ }
} finally {
cce.EndExpose();
}
@@ -97,9 +102,13 @@ namespace VC { VCExpr C = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr);
if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {
return gen.Implies(C, N);
- } else {
+ }
+ else {
int id = ac.UniqueId;
- ctxt.Label2absy[id] = ac;
+ if (ctxt.Label2absy != null) {
+ ctxt.Label2absy[id] = ac;
+ }
+
switch (Subsumption(ac)) {
case CommandLineOptions.SubsumptionOption.Never:
break;
@@ -112,25 +121,31 @@ namespace VC { }
break;
default:
- Contract.Assert(false);throw new cce.UnreachableException(); // unexpected case
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected case
}
-
+
// (MSchaef) Hack: This line might be useless, but at least it is not harmful
// need to test it
- if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed)
+ if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed)
return gen.Implies(C, N);
-
- if (ctxt.ControlFlowVariable != null)
- {
+
+ if (ctxt.ControlFlowVariable == null) {
+ Contract.Assert(ctxt.Label2absy != null);
+ return gen.AndSimp(gen.LabelNeg(cce.NonNull(id.ToString()), C), N);
+ }
+ else {
VCExpr controlFlowVariableExpr = ctxt.Ctxt.BoogieExprTranslator.LookupVariable(ctxt.ControlFlowVariable);
Contract.Assert(controlFlowVariableExpr != null);
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));
+ if (ctxt.Label2absy == null) {
+ return gen.AndSimp(gen.Implies(assertFailure, C), gen.Implies(C, N));
+ }
+ else {
+ return gen.AndSimp(gen.LabelNeg(cce.NonNull(id.ToString()), gen.Implies(assertFailure, C)), gen.Implies(C, N));
+ }
}
- else
- return gen.AndSimp(gen.LabelNeg(cce.NonNull(id.ToString()), C), N);
}
} else if (cmd is AssumeCmd) {
|