summaryrefslogtreecommitdiff
path: root/Source/Concurrency/OwickiGries.cs
diff options
context:
space:
mode:
authorGravatar qadeer <unknown>2014-04-15 09:32:38 -0700
committerGravatar qadeer <unknown>2014-04-15 09:32:38 -0700
commit72b5d281e554cb980155fcc971717e954e921a60 (patch)
treee665a6bc07dfd92f8ad9afdbb54ed9c4a2787c77 /Source/Concurrency/OwickiGries.cs
parent96fae84963c1e84ad70a576e97648e1b3c2d3087 (diff)
added more types to constructed expressions
Diffstat (limited to 'Source/Concurrency/OwickiGries.cs')
-rw-r--r--Source/Concurrency/OwickiGries.cs8
1 files changed, 5 insertions, 3 deletions
diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index 6c78f80d..b5d41b21 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -386,7 +386,8 @@ namespace Microsoft.Boogie
Expr bb = Expr.True;
foreach (Variable o in ogOldGlobalMap.Keys)
{
- bb = Expr.Binary(BinaryOperator.Opcode.And, bb, Expr.Eq(Expr.Ident(o), Expr.Ident(ogOldGlobalMap[o])));
+ bb = Expr.And(bb, Expr.Eq(Expr.Ident(o), Expr.Ident(ogOldGlobalMap[o])));
+ bb.Type = Type.Bool;
}
return bb;
}
@@ -783,6 +784,7 @@ namespace Microsoft.Boogie
foreach (AssertCmd assertCmd in actionInfo.thisGate)
{
alphaExpr = Expr.And(alphaExpr, assertCmd.Expr);
+ alphaExpr.Type = Type.Bool;
}
alpha = Substituter.Apply(always, alphaExpr);
foreach (Variable f in impl.OutParams)
@@ -955,11 +957,11 @@ namespace Microsoft.Boogie
}
foreach (string domainName in linearTypeChecker.linearDomains.Keys)
{
- newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Binary(BinaryOperator.Opcode.Eq, Expr.Ident(domainNameToLocalVar[domainName]), domainNameToExpr[domainName])));
+ newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Eq(Expr.Ident(domainNameToLocalVar[domainName]), domainNameToExpr[domainName])));
}
foreach (Variable v in ogOldGlobalMap.Keys)
{
- newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Binary(BinaryOperator.Opcode.Eq, Expr.Ident(v), Expr.Ident(ogOldGlobalMap[v]))));
+ newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Eq(Expr.Ident(v), Expr.Ident(ogOldGlobalMap[v]))));
}
newCmds.AddRange(header.Cmds);
header.Cmds = newCmds;