diff options
| author |  qadeer <unknown> | 2013-07-15 00:17:44 -0700 |
|---|---|---|
| committer | qadeer <unknown> | 2013-07-15 00:17:44 -0700 |
| commit | 100518bf2d57bd48d5dd24c7a7bf0ee86daeb424 (patch) | |
| tree | 6c063083f6a9fdc72921bc787e052afe54f4ab32 /Source/Core | |
| parent | 4ef06586c73b8337c87d6b129315365b6ed6d96b (diff) | |
end atomic actions at async and parallel calls
Diffstat (limited to 'Source/Core')
| -rw-r--r-- | Source/Core/OwickiGries.cs | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs index 14f5f328..e353700f 100644 --- a/Source/Core/OwickiGries.cs +++ b/Source/Core/OwickiGries.cs @@ -131,7 +131,7 @@ namespace Microsoft.Boogie public override Cmd VisitCallCmd(CallCmd node)
{
ProcedureInfo info = procNameToInfo[node.callee];
- if (!node.IsAsync && !info.isAtomic)
+ if (node.InParallelWith != null || node.IsAsync || !info.isAtomic)
{
procNameToInfo[currentImpl.Name].isAtomic = false;
moreProcessingRequired = true;
@@ -487,6 +487,10 @@ namespace Microsoft.Boogie CallCmd callCmd = cmd as CallCmd;
if (callCmd != null)
{
+ if (callCmd.InParallelWith != null || callCmd.IsAsync || !procNameToInfo[callCmd.callee].isAtomic)
+ {
+ AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar);
+ }
if (callCmd.InParallelWith != null)
{
List<Expr> ins;
@@ -507,14 +511,12 @@ namespace Microsoft.Boogie dummyCallCmd.Proc = dummyAsyncTargetProc;
newCmds.Add(dummyCallCmd);
}
- else if (procNameToInfo[callCmd.callee].isAtomic)
+ else
{
newCmds.Add(callCmd);
}
- else
+ if (callCmd.InParallelWith != null || callCmd.IsAsync || !procNameToInfo[callCmd.callee].isAtomic)
{
- AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar);
- newCmds.Add(callCmd);
HashSet<Variable> availableLocalLinearVars = new HashSet<Variable>(linearTypechecker.availableLocalLinearVars[callCmd]);
foreach (IdentifierExpr ie in callCmd.Outs)
{
|