From b06cff3aa1491d0b2e5885a6e801c1d924af2e11 Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Wed, 4 Sep 2013 15:07:23 -0700
Subject: fixed the linear type checking related to globals fixed the modset
 analysis so that it infers the stable predicate also added more information
 to type error messages

---
 Source/Core/DeadVarElim.cs | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'Source/Core/DeadVarElim.cs')

diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index 11927293..900546e6 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);
-- 
cgit v1.2.3