simplified yield type chcking and added treiber stack (not fully done)

1 files changed, 25 insertions, 0 deletions

diff --git a/Source/Concurrency/LinearSets.cs b/Source/Concurrency/LinearSets.cs
index fc44468c..6675e809 100644
--- a/Source/Concurrency/LinearSets.cs
+++ b/Source/Concurrency/LinearSets.cs
@@ -154,6 +154,16 @@ namespace Microsoft.Boogie
         }

         public override Implementation VisitImplementation(Implementation node)

         {

+            node.PruneUnreachableBlocks();

+            node.ComputePredecessorsForBlocks();

+            GraphUtil.Graph<Block> graph = Program.GraphFromImpl(node);

+            graph.ComputeLoops();

+            if (!graph.Reducible)

+            {

+                Error(node, "A loop in the implementation is not reducible");

+                return node;

+            }

+

             HashSet<Variable> start = new HashSet<Variable>(globalVarToDomainName.Keys);

             for (int i = 0; i < node.InParams.Count; i++)

             {

@@ -223,6 +233,15 @@ namespace Microsoft.Boogie
                     }

                 }

             }

+

+            foreach (Block header in graph.Headers)

+            {

+                foreach (GlobalVariable g in globalVarToDomainName.Keys.Except(availableLinearVars[header]))

+                {

+                    Error(header, string.Format("Global variable {0} must be available at a loop head", g.Name));

+                }

+            }

+

             return impl;

         }

         public void AddAvailableVars(CallCmd callCmd, HashSet<Variable> start)

@@ -566,6 +585,12 @@ namespace Microsoft.Boogie
                 var domainName = FindDomainName(v);

                 domainNameToScope[domainName].Add(v);

             }

+            foreach (Variable v in program.GlobalVariables())

+            {

+                var domainName = FindDomainName(v);

+                if (domainName == null) continue;

+                domainNameToScope[domainName].Add(v);

+            }

             foreach (string domainName in linearDomains.Keys)

             {

                 newCmds.Add(new AssumeCmd(Token.NoToken, DisjointnessExpr(domainName, domainNameToInputVar[domainName], domainNameToScope[domainName])));