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

1 files changed, 7 insertions, 0 deletions

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);