diff options
| author |  akashlal <akashl@AKASHL-LT.fareast.corp.microsoft.com> | 2015-06-01 10:39:14 +0530 |
|---|---|---|
| committer | akashlal <akashl@AKASHL-LT.fareast.corp.microsoft.com> | 2015-06-01 10:39:14 +0530 |
| commit | c8eb509045eccd1b44fd335f9e1ef5cf80d7cd89 (patch) | |
| tree | ed29a4cbce3e8b88fe2fddb207eeb790b1a657e4 /Source | |
| parent | dfaac23736f142a4c66a8457f7a4be99b245cb98 (diff) | |
| parent | 2d2774f8aacf0e79765d6c59db4cf16c15676aef (diff) | |
Merge branch 'master' of https://github.com/boogie-org/boogie
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Concurrency/OwickiGries.cs | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs index dbd1dcbd..626f2c4a 100644 --- a/Source/Concurrency/OwickiGries.cs +++ b/Source/Concurrency/OwickiGries.cs @@ -919,6 +919,15 @@ namespace Microsoft.Boogie {
HashSet<Variable> availableLinearVars = new HashSet<Variable>(AvailableLinearVars(callCmd));
linearTypeChecker.AddAvailableVars(callCmd, availableLinearVars);
+
+ if (!callCmd.IsAsync && globalMods.Count > 0 && pc != null)
+ {
+ // assume pc || alpha(i, g);
+ Expr assumeExpr = Expr.Or(Expr.Ident(pc), alpha);
+ assumeExpr.Type = Type.Bool;
+ newCmds.Add(new AssumeCmd(Token.NoToken, assumeExpr));
+ }
+
Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(availableLinearVars, domainNameToInputVar);
AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);
}
@@ -930,6 +939,15 @@ namespace Microsoft.Boogie DesugarParallelCallCmd(newCmds, parCallCmd);
HashSet<Variable> availableLinearVars = new HashSet<Variable>(AvailableLinearVars(parCallCmd));
linearTypeChecker.AddAvailableVars(parCallCmd, availableLinearVars);
+
+ if (globalMods.Count > 0 && pc != null)
+ {
+ // assume pc || alpha(i, g);
+ Expr assumeExpr = Expr.Or(Expr.Ident(pc), alpha);
+ assumeExpr.Type = Type.Bool;
+ newCmds.Add(new AssumeCmd(Token.NoToken, assumeExpr));
+ }
+
Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(availableLinearVars, domainNameToInputVar);
AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);
}
|