summaryrefslogtreecommitdiff
path: root/Source/Concurrency/OwickiGries.cs
diff options
context:
space:
mode:
authorGravatar qadeer <unknown>2014-05-07 09:37:42 -0700
committerGravatar qadeer <unknown>2014-05-07 09:37:42 -0700
commitb53684a200816f84772a5627932d700a5eda1b97 (patch)
treee308a4af3bfceca8991ed904f84259a4334e7ac1 /Source/Concurrency/OwickiGries.cs
parent62addf3f3529ec79681bf0a4fdf5c57872aca294 (diff)
a bug fix
Diffstat (limited to 'Source/Concurrency/OwickiGries.cs')
-rw-r--r--Source/Concurrency/OwickiGries.cs20
1 files changed, 16 insertions, 4 deletions
diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index 67e69cdd..c99d3507 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -353,12 +353,16 @@ namespace Microsoft.Boogie
Expr bb = OldEqualityExpr(ogOldGlobalMap);
// assert pc || g_old == g || beta(i, g_old, o, g);
- AssertCmd skipOrBetaAssertCmd = new AssertCmd(tok, Expr.Or(Expr.Ident(pc), Expr.Or(aa, beta)));
+ Expr assertExpr = Expr.Or(Expr.Ident(pc), Expr.Or(aa, beta));
+ assertExpr.Typecheck(new TypecheckingContext(null));
+ AssertCmd skipOrBetaAssertCmd = new AssertCmd(tok, assertExpr);
skipOrBetaAssertCmd.ErrorData = "Transition invariant in initial state violated";
newCmds.Add(skipOrBetaAssertCmd);
// assert pc ==> o_old == o && g_old == g;
- AssertCmd skipAssertCmd = new AssertCmd(tok, Expr.Imp(Expr.Ident(pc), bb));
+ assertExpr = Expr.Imp(Expr.Ident(pc), bb);
+ assertExpr.Typecheck(new TypecheckingContext(null));
+ AssertCmd skipAssertCmd = new AssertCmd(tok, assertExpr);
skipAssertCmd.ErrorData = "Transition invariant in final state violated"; ;
newCmds.Add(skipAssertCmd);
@@ -373,6 +377,10 @@ namespace Microsoft.Boogie
Expr.Imp(aa, Expr.Ident(pc)),
Expr.Or(Expr.Ident(ok), beta)
});
+ foreach (Expr e in pcUpdateRHS)
+ {
+ e.Typecheck(new TypecheckingContext(null));
+ }
newCmds.Add(new AssignCmd(Token.NoToken, pcUpdateLHS, pcUpdateRHS));
}
}
@@ -458,7 +466,9 @@ namespace Microsoft.Boogie
if (pc != null)
{
// assume pc || alpha(i, g);
- newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Or(Expr.Ident(pc), alpha)));
+ Expr assumeExpr = Expr.Or(Expr.Ident(pc), alpha);
+ assumeExpr.Type = Type.Bool;
+ newCmds.Add(new AssumeCmd(Token.NoToken, assumeExpr));
}
}
@@ -898,7 +908,9 @@ namespace Microsoft.Boogie
if (globalMods.Count > 0 && pc != null)
{
// assume pc || alpha(i, g);
- newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Or(Expr.Ident(pc), alpha)));
+ Expr assumeExpr = Expr.Or(Expr.Ident(pc), alpha);
+ assumeExpr.Type = Type.Bool;
+ newCmds.Add(new AssumeCmd(Token.NoToken, assumeExpr));
}
HashSet<Variable> availableLinearVars = new HashSet<Variable>(AvailableLinearVars(parCallCmd));
linearTypeChecker.AddAvailableVars(parCallCmd, availableLinearVars);