diff options
author | Pantazis Deligiannis <pdeligia@me.com> | 2013-10-09 22:20:01 +0100 |
---|---|---|
committer | Pantazis Deligiannis <pdeligia@me.com> | 2013-10-09 22:20:01 +0100 |
commit | 37a8b374462a3f41d43546da75ae540cc75a329d (patch) | |
tree | 8f3ae7b0f2d58855971e499f2891fe72045551ec /Source/Core/DeadVarElim.cs | |
parent | e3e9aff76e22d05cdb3c558c8106d4a201aa0141 (diff) | |
parent | 225f211c0b94ad3d13dee857596f322b666fe259 (diff) |
Merge
Diffstat (limited to 'Source/Core/DeadVarElim.cs')
-rw-r--r-- | Source/Core/DeadVarElim.cs | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs index f3056e4f..cb6ce689 100644 --- a/Source/Core/DeadVarElim.cs +++ b/Source/Core/DeadVarElim.cs @@ -42,6 +42,7 @@ namespace Microsoft.Boogie { static Procedure enclosingProc;
static Dictionary<Procedure/*!*/, HashSet<Variable/*!*/>/*!*/>/*!*/ modSets;
static HashSet<Procedure> yieldingProcs;
+ static HashSet<Procedure> asyncAndParallelCallTargetProcs;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullDictionaryAndValues(modSets));
@@ -69,6 +70,7 @@ namespace Microsoft.Boogie { modSets = new Dictionary<Procedure/*!*/, HashSet<Variable/*!*/>/*!*/>();
yieldingProcs = new HashSet<Procedure>();
+ asyncAndParallelCallTargetProcs = new HashSet<Procedure>();
HashSet<Procedure/*!*/> implementedProcs = new HashSet<Procedure/*!*/>();
foreach (Declaration/*!*/ decl in program.TopLevelDeclarations) {
@@ -118,6 +120,10 @@ namespace Microsoft.Boogie { {
x.AddAttribute("yields");
}
+ if (asyncAndParallelCallTargetProcs.Contains(x) && !QKeyValue.FindBoolAttribute(x.Attributes, "stable"))
+ {
+ x.AddAttribute("stable");
+ }
}
if (false /*CommandLineOptions.Clo.Trace*/) {
@@ -209,6 +215,7 @@ namespace Microsoft.Boogie { var curr = callCmd;
while (curr != null)
{
+ asyncAndParallelCallTargetProcs.Add(curr.Proc);
if (!yieldingProcs.Contains(curr.Proc))
{
yieldingProcs.Add(curr.Proc);
|