Merge

2 files changed, 29 insertions, 22 deletions

diff --git a/Source/GPUVerify/RaceInstrumenterBase.cs b/Source/GPUVerify/RaceInstrumenterBase.cs
index 5155b192..13a4585b 100644
--- a/Source/GPUVerify/RaceInstrumenterBase.cs
+++ b/Source/GPUVerify/RaceInstrumenterBase.cs
@@ -456,7 +456,7 @@ namespace GPUVerify
                .Select(ofs => verifier.varDefAnalyses[impl].SubstDualisedDefinitions(ofs, 1, impl.Name))

                .ToList();

 

-            if (!offsets.Contains(null))

+            if (offsets.Count != 0 && !offsets.Contains(null))

             {

                 AddAccessedOffsetsAreConstantCandidateInvariant(region, v, offsets, accessType);

             }

diff --git a/Source/VCGeneration/BlockPredicator.cs b/Source/VCGeneration/BlockPredicator.cs
index 7ce38fd3..040d3a5b 100644
--- a/Source/VCGeneration/BlockPredicator.cs
+++ b/Source/VCGeneration/BlockPredicator.cs
@@ -70,20 +70,20 @@ public class BlockPredicator {
                        new IfThenElse(Token.NoToken),
                        new ExprSeq(p, rhs, lhs.AsExpr))))));
     } else if (cmd is AssertCmd) {
-      var aCmd = (AssertCmd)cmd;

+      var aCmd = (AssertCmd)cmd;
       if (cmdSeq.Last() is AssignCmd &&
           cmdSeq.Cast<Cmd>().SkipEnd(1).All(c => c is AssertCmd)) {
         // This may be a loop invariant.  Make sure it continues to appear as
         // the first statement in the block.
         var assign = cmdSeq.Last();
-        cmdSeq.Truncate(cmdSeq.Length-1);

-        aCmd.Expr = Expr.Imp(pExpr, aCmd.Expr);

-        cmdSeq.Add(aCmd);

+        cmdSeq.Truncate(cmdSeq.Length-1);
+        aCmd.Expr = Expr.Imp(pExpr, aCmd.Expr);
+        cmdSeq.Add(aCmd);
         // cmdSeq.Add(new AssertCmd(aCmd.tok, Expr.Imp(pExpr, aCmd.Expr)));
         cmdSeq.Add(assign);
-      } else {

-        aCmd.Expr = Expr.Imp(p, aCmd.Expr);

-        cmdSeq.Add(aCmd);

+      } else {
+        aCmd.Expr = Expr.Imp(p, aCmd.Expr);
+        cmdSeq.Add(aCmd);
         // cmdSeq.Add(new AssertCmd(aCmd.tok, Expr.Imp(p, aCmd.Expr)));
       }
     } else if (cmd is AssumeCmd) {
@@ -117,10 +117,17 @@ public class BlockPredicator {
       Debug.Assert(useProcedurePredicates);
       var cCmd = (CallCmd)cmd;
       cCmd.Ins.Insert(0, p);
-      cmdSeq.Add(cCmd);

-    }

-    else if (cmd is CommentCmd) {

-      // skip

+      cmdSeq.Add(cCmd);
+    }
+    else if (cmd is CommentCmd) {
+      // skip
+      } else if (cmd is StateCmd) {
+      var sCmd = (StateCmd)cmd;
+      var newCmdSeq = new CmdSeq();
+      foreach (Cmd c in sCmd.Cmds)
+        PredicateCmd(newCmdSeq, c);
+      sCmd.Cmds = newCmdSeq;
+      cmdSeq.Add(sCmd);
     } else {
       Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString());
     }
@@ -163,12 +170,12 @@ public class BlockPredicator {
     }
   }
 
-  void PredicateImplementation() {

-    try {

-      blockGraph = prog.ProcessLoops(impl);

-    }

-    catch (Program.IrreducibleLoopException) {

-      return;

+  void PredicateImplementation() {
+    try {
+      blockGraph = prog.ProcessLoops(impl);
+    }
+    catch (Program.IrreducibleLoopException) {
+      return;
     }
     var sortedBlocks = blockGraph.LoopyTopSort();
 
@@ -308,10 +315,10 @@ public class BlockPredicator {
       if (impl != null)
         new BlockPredicator(p, impl, createCandidateInvariants, useProcedurePredicates).PredicateImplementation();
     }
-  }

-

-  public static void Predicate(Program p, Implementation impl) {

-    new BlockPredicator(p, impl, false, false).PredicateImplementation();

+  }
+
+  public static void Predicate(Program p, Implementation impl) {
+    new BlockPredicator(p, impl, false, false).PredicateImplementation();
   }
 
 }