summaryrefslogtreecommitdiff
path: root/Source/Concurrency/OwickiGries.cs
diff options
context:
space:
mode:
authorGravatar qadeer <unknown>2014-04-25 16:47:36 -0700
committerGravatar qadeer <unknown>2014-04-25 16:47:36 -0700
commit1a114f457299c87f9e9548992659ffc726fe5e7a (patch)
treefe1e6b9c3d79d8547c22db8fb5a7f44315f5b5ce /Source/Concurrency/OwickiGries.cs
parentb17515ca23fc7f5ae1fb8e6642366f761d0eeacf (diff)
updated the mover checks
Diffstat (limited to 'Source/Concurrency/OwickiGries.cs')
-rw-r--r--Source/Concurrency/OwickiGries.cs14
1 files changed, 13 insertions, 1 deletions
diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index b646e8cf..9ec07854 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -1283,7 +1283,19 @@ namespace Microsoft.Boogie
duplicateProc.Modifies = new List<IdentifierExpr>();
program.GlobalVariables().Iter(x => duplicateProc.Modifies.Add(Expr.Ident(x)));
CodeExpr action = (CodeExpr)duplicator.VisitCodeExpr(moverTypeChecker.procToActionInfo[proc].thisAction);
- Implementation impl = new Implementation(Token.NoToken, duplicateProc.Name, proc.TypeParameters, proc.InParams, proc.OutParams, action.LocVars, action.Blocks);
+
+ List<Cmd> cmds = new List<Cmd>();
+ foreach (AssertCmd assertCmd in moverTypeChecker.procToActionInfo[proc].thisGate)
+ {
+ cmds.Add(new AssumeCmd(Token.NoToken, (Expr)duplicator.Visit(assertCmd.Expr)));
+ }
+ Block newInitBlock = new Block(Token.NoToken, "_init", cmds,
+ new GotoCmd(Token.NoToken, new List<string>(new string[] { action.Blocks[0].Label }),
+ new List<Block>(new Block[] { action.Blocks[0] })));
+ List<Block> newBlocks = new List<Block>();
+ newBlocks.Add(newInitBlock);
+ newBlocks.AddRange(action.Blocks);
+ Implementation impl = new Implementation(Token.NoToken, duplicateProc.Name, proc.TypeParameters, proc.InParams, proc.OutParams, action.LocVars, newBlocks);
impl.Proc = duplicateProc;
impl.Proc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
impl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));