diff options
| author |  Unknown <qadeer@GHALIB.redmond.corp.microsoft.com> | 2012-02-23 13:52:02 -0800 |
|---|---|---|
| committer | Unknown <qadeer@GHALIB.redmond.corp.microsoft.com> | 2012-02-23 13:52:02 -0800 |
| commit | dc8e43c41b46e8d2ae9bc93caa97f7b7d891b5df (patch) | |
| tree | be54b512a45481d6164f7127664be66a0ce1652d /Source/VCGeneration/VC.cs | |
| parent | 51e9ec1d1b9fd9d707a7eb5b9c903e266efbdad1 (diff) | |
using model instead of labels
Diffstat (limited to 'Source/VCGeneration/VC.cs')
| -rw-r--r-- | Source/VCGeneration/VC.cs | 17 |
1 files changed, 16 insertions, 1 deletions
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 6026b862..49fa7144 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1536,9 +1536,24 @@ namespace VC { }
));
- VCExpr vc = parent.GenerateVCAux(impl, null, label2absy, checker);
+ 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);
+ }
+
+ VCExpr vc = parent.GenerateVCAux(impl, controlFlowVariable, label2absy, checker);
Contract.Assert(vc != null);
+ if (!CommandLineOptions.Clo.UseLabels) {
+ VCExpr controlFlowVariableExpr = bet.LookupVariable(controlFlowVariable);
+ Contract.Assert(controlFlowVariableExpr != null);
+ 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);
+ }
+
if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) {
reporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback, mvInfo, parent.implName2LazyInliningInfo, cce.NonNull(this.Checker.TheoremProver.Context), parent.program);
} else {
|