Merge

28 files changed, 727 insertions, 605 deletions

diff --git a/Chalice/tests/examples/list-reverse.chalice b/Chalice/tests/examples/list-reverse.chalice
new file mode 100644
index 00000000..c694b4c9
--- /dev/null
+++ b/Chalice/tests/examples/list-reverse.chalice
@@ -0,0 +1,44 @@
+class Node {

+  var next : Node;

+  var val : int;

+

+  predicate list {

+    acc(next) && acc(val) && (next!=null ==> next.list)

+  }

+  

+  function vals() : seq<int>

+    requires list

+  {

+    unfolding list in (next == null ? [val] : [val] ++ next.vals())

+  }

+

+  function reverse_vals() : seq<int>

+    requires list

+  {

+    unfolding list in (next == null ? [val] : next.reverse_vals() ++ [val])

+  }

+

+  method reverse_in_place() returns (r:Node)

+    requires list;

+    ensures r != null && r.list;

+    ensures r.vals() == old(this.reverse_vals());

+  {

+    var l : Node := this;

+    r := null;

+

+    while (l != null) 

+      invariant l!=null ==> l.list;

+      invariant r!=null ==> r.list;

+      invariant old(this.reverse_vals()) == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());

+    { 

+      var y: Node;

+      unfold l.list;

+    

+      y := l.next;

+      l.next := r;

+      r := l;

+      fold r.list;

+      l := y;

+    }

+  }

+}
\ No newline at end of file
diff --git a/Chalice/tests/predicates/list-reverse.output.txt b/Chalice/tests/examples/list-reverse.output.txt
index d8e19122..d8e19122 100644
--- a/Chalice/tests/predicates/list-reverse.output.txt
+++ b/Chalice/tests/examples/list-reverse.output.txt
diff --git a/Chalice/tests/predicates/list-reverse.chalice b/Chalice/tests/predicates/list-reverse.chalice
deleted file mode 100644
index 5a596409..00000000
--- a/Chalice/tests/predicates/list-reverse.chalice
+++ /dev/null
@@ -1,158 +0,0 @@
-// this would be nice in the "examples" folder (at least, the version without the commented blocks), once the problem with old(..) is fixed

-

-class Node {

-  var next : Node;

-  var val : int;

-

-  predicate list {

-    acc(next) && acc(val) && (next!=null ==> next.list)

-  }

-  

-  function vals() : seq<int>

-    requires list

-  {

-    unfolding list in (next == null ? [val] : [val] ++ next.vals())

-  }

-

-  function reverse_vals() : seq<int>

-    requires list

-  {

-    unfolding list in (next == null ? [val] : next.reverse_vals() ++ [val])

-  }

-

-  method reverse_in_place() returns (r:Node)

-    requires list;

-    ensures true;

-  {

-    var l : Node := this;

-    r := null;

-

-    var rev : seq<int> := this.reverse_vals(); // cached here, because old(this.reverse_vals()) doesn't work properly

-    

-    while (l != null) 

-      invariant l!=null ==> l.list;

-      invariant r!=null ==> r.list;

-      invariant rev == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());

-    { 

-      var y: Node;

-//      if (r != null) {

-//        unfold r.list; fold r.list;

-//      }

-      unfold l.list;

-//      if (l.next != null) {

-//        unfold l.next.list; fold l.next.list;

-//      }

-    

-      y := l.next;

-      l.next := r;

-      r := l;

-      fold r.list;

-      l := y;

-    }

-    assert r.vals() == rev; // should be the post-condition

-  }

-  

-

-   method reverse_in_place_01() returns (r:Node)

-    requires list;

-    ensures true;

-  {

-    var l : Node := this;

-    r := null;

-

-    var rev : seq<int> := this.reverse_vals(); // cached here, because old(this.reverse_vals()) doesn't work properly

-    

-    while (l != null) 

-      invariant l!=null ==> l.list;

-      invariant r!=null ==> r.list;

-      invariant rev == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());

-    { 

-      var y: Node;

-//      if (r != null) {

-//        unfold r.list; fold r.list;

-//      }

-      unfold l.list;

-      if (l.next != null) {

-        unfold l.next.list; fold l.next.list;

-      }

-    

-      y := l.next;

-      l.next := r;

-      r := l;

-      fold r.list;

-      l := y;

-    }

-    assert r.vals() == rev; // should be the post-condition

-  }

-  

-   

-

-   method reverse_in_place_10() returns (r:Node)

-    requires list;

-    ensures true;

-  {

-    var l : Node := this;

-    r := null;

-

-    var rev : seq<int> := this.reverse_vals(); // cached here, because old(this.reverse_vals()) doesn't work properly

-    

-    while (l != null) 

-      invariant l!=null ==> l.list;

-      invariant r!=null ==> r.list;

-      invariant rev == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());

-    { 

-      var y: Node;

-      if (r != null) {

-        unfold r.list; fold r.list;

-      }

-      unfold l.list;

-//      if (l.next != null) {

-//        unfold l.next.list; fold l.next.list;

-//      }

-    

-      y := l.next;

-      l.next := r;

-      r := l;

-      fold r.list;

-      l := y;

-    }

-    assert r.vals() == rev; // should be the post-condition

-  }

-  

-   

-

-

-   method reverse_in_place_11() returns (r:Node)

-    requires list;

-    ensures true;

-  {

-    var l : Node := this;

-    r := null;

-

-    var rev : seq<int> := this.reverse_vals(); // cached here, because old(this.reverse_vals()) doesn't work properly

-    

-    while (l != null) 

-      invariant l!=null ==> l.list;

-      invariant r!=null ==> r.list;

-      invariant rev == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());

-    { 

-      var y: Node;

-      if (r != null) {

-        unfold r.list; fold r.list;

-      }

-      unfold l.list;

-      if (l.next != null) {

-        unfold l.next.list; fold l.next.list;

-      }

-    

-      y := l.next;

-      l.next := r;

-      r := l;

-      fold r.list;

-      l := y;

-    }

-    assert r.vals() == rev; // should be the post-condition

-  }

-  

-   

-}
\ No newline at end of file
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 61943cf0..0911cbd3 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -404,7 +404,7 @@ namespace Microsoft.Boogie {
             inline = true;

           }

         }

-        if (inline && CommandLineOptions.Clo.StratifiedInlining == 0) {

+        if (inline) {

           foreach (var d in TopLevelDeclarations) {

             var impl = d as Implementation;

             if (impl != null) {

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 704c5973..90cfd6d8 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -2482,6 +2482,10 @@ namespace Microsoft.Boogie {
           }

         }

 

+        if (CommandLineOptions.Clo.StratifiedInlining > 0) {

+          return !QKeyValue.FindBoolAttribute(Attributes, "entrypoint");

+        }

+

         return false;

       }

     }

diff --git a/Source/GPUVerify/BlockPredicator.cs b/Source/GPUVerify/BlockPredicator.cs
new file mode 100644
index 00000000..15ad2432
--- /dev/null
+++ b/Source/GPUVerify/BlockPredicator.cs
@@ -0,0 +1,191 @@
+using Microsoft.Boogie;
+using System;
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using System.Linq;
+
+namespace GPUVerify {
+
+class BlockPredicator {
+
+  Program prog;
+  Implementation impl;
+
+  Expr returnBlockId;
+
+  LocalVariable curVar, pVar;
+  IdentifierExpr cur, p;
+  Expr pExpr;
+  Dictionary<Microsoft.Boogie.Type, IdentifierExpr> havocVars =
+    new Dictionary<Microsoft.Boogie.Type, IdentifierExpr>();
+  Dictionary<Block, Expr> blockIds = new Dictionary<Block, Expr>();
+
+  BlockPredicator(Program p, Implementation i) {
+    prog = p;
+    impl = i;
+  }
+
+  void PredicateCmd(CmdSeq cmdSeq, Cmd cmd) {
+    if (cmd is AssignCmd) {
+      var aCmd = (AssignCmd)cmd;
+      cmdSeq.Add(new AssignCmd(Token.NoToken, aCmd.Lhss,
+                   new List<Expr>(aCmd.Lhss.Zip(aCmd.Rhss, (lhs, rhs) =>
+                     new NAryExpr(Token.NoToken,
+                       new IfThenElse(Token.NoToken),
+                       new ExprSeq(p, rhs, lhs.AsExpr))))));
+    } else if (cmd is AssertCmd) {
+      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);
+        cmdSeq.Add(new AssertCmd(Token.NoToken, Expr.Imp(pExpr, aCmd.Expr)));
+        cmdSeq.Add(assign);
+      } else {
+        cmdSeq.Add(new AssertCmd(Token.NoToken, Expr.Imp(p, aCmd.Expr)));
+      }
+    } else if (cmd is AssumeCmd) {
+      var aCmd = (AssumeCmd)cmd;
+      cmdSeq.Add(new AssumeCmd(Token.NoToken, Expr.Imp(p, aCmd.Expr)));
+    } else if (cmd is HavocCmd) {
+      var hCmd = (HavocCmd)cmd;
+      foreach (IdentifierExpr v in hCmd.Vars) {
+        Microsoft.Boogie.Type type = v.Decl.TypedIdent.Type;
+        Contract.Assert(type != null);
+
+        IdentifierExpr havocTempExpr;
+        if (havocVars.ContainsKey(type)) {
+          havocTempExpr = havocVars[type];
+        } else {
+          var havocVar = new LocalVariable(Token.NoToken,
+                             new TypedIdent(Token.NoToken,
+                                            "_HAVOC_" + type.ToString(), type));
+          impl.LocVars.Add(havocVar);
+          havocVars[type] = havocTempExpr =
+            new IdentifierExpr(Token.NoToken, havocVar);
+        }
+        cmdSeq.Add(new HavocCmd(Token.NoToken,
+                                new IdentifierExprSeq(havocTempExpr)));
+        cmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, v,
+                                    new NAryExpr(Token.NoToken,
+                                      new IfThenElse(Token.NoToken),
+                                      new ExprSeq(p, havocTempExpr, v))));
+      }
+    } else if (cmd is CallCmd) {
+      var cCmd = (CallCmd)cmd;
+      cCmd.Ins.Insert(0, p);
+      cmdSeq.Add(cCmd);
+    } else {
+      Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString());
+    }
+  }
+
+  void PredicateTransferCmd(CmdSeq cmdSeq, TransferCmd cmd) {
+    if (cmd is GotoCmd) {
+      var gCmd = (GotoCmd)cmd;
+      var targets = new List<Expr>(
+        gCmd.labelTargets.Cast<Block>().Select(b => blockIds[b]));
+      if (targets.Count == 1) {
+        PredicateCmd(cmdSeq, Cmd.SimpleAssign(Token.NoToken, cur, targets[0]));
+      } else {
+        PredicateCmd(cmdSeq, new HavocCmd(Token.NoToken,
+                                          new IdentifierExprSeq(cur)));
+        PredicateCmd(cmdSeq, new AssumeCmd(Token.NoToken,
+               targets.Select(t => (Expr)Expr.Eq(cur, t)).Aggregate(Expr.Or)));
+      }
+    } else if (cmd is ReturnCmd) {
+      PredicateCmd(cmdSeq, Cmd.SimpleAssign(Token.NoToken, cur, returnBlockId));
+    } else {
+      Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString());
+    }
+  }
+
+  void PredicateImplementation() {
+    var g = prog.ProcessLoops(impl);
+    var sortedBlocks = g.LoopyTopSort();
+
+    int blockId = 0;
+    foreach (var block in impl.Blocks)
+      blockIds[block] = Expr.Literal(blockId++);
+    returnBlockId = Expr.Literal(blockId++);
+
+    curVar = new LocalVariable(Token.NoToken,
+                               new TypedIdent(Token.NoToken, "cur",
+                                              Microsoft.Boogie.Type.Int));
+    impl.LocVars.Add(curVar);
+    cur = Expr.Ident(curVar);
+
+    pVar = new LocalVariable(Token.NoToken,
+                             new TypedIdent(Token.NoToken, "p",
+                                            Microsoft.Boogie.Type.Bool));
+    impl.LocVars.Add(pVar);
+    p = Expr.Ident(pVar);
+
+    var newBlocks = new List<Block>();
+
+    var fp = Expr.Ident(impl.InParams[0]);
+    Block entryBlock = new Block();
+    entryBlock.Label = "entry";
+    entryBlock.Cmds = new CmdSeq(Cmd.SimpleAssign(Token.NoToken, cur,
+                        new NAryExpr(Token.NoToken,
+                          new IfThenElse(Token.NoToken),
+                          new ExprSeq(fp, blockIds[sortedBlocks[0].Item1],
+                                      returnBlockId))));
+    newBlocks.Add(entryBlock);
+
+    var prevBlock = entryBlock;
+    foreach (var n in sortedBlocks) {
+      if (n.Item2) {
+        var tailBlock = new Block();
+        newBlocks.Add(tailBlock);
+
+        tailBlock.Label = n.Item1.Label + ".tail";
+        tailBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken,
+                                             Expr.Neq(cur, blockIds[n.Item1])));
+
+        prevBlock.TransferCmd = new GotoCmd(Token.NoToken,
+                                            new BlockSeq(tailBlock, n.Item1));
+        prevBlock = tailBlock;
+      } else {
+        var runBlock = n.Item1;
+        newBlocks.Add(runBlock);
+
+        pExpr = Expr.Eq(cur, blockIds[runBlock]);
+        CmdSeq newCmdSeq = new CmdSeq();
+        newCmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, p, pExpr));
+        foreach (Cmd cmd in runBlock.Cmds)
+          PredicateCmd(newCmdSeq, cmd);
+        PredicateTransferCmd(newCmdSeq, runBlock.TransferCmd);
+        runBlock.Cmds = newCmdSeq;
+
+        prevBlock.TransferCmd = new GotoCmd(Token.NoToken,
+                                            new BlockSeq(runBlock));
+        prevBlock = runBlock;
+      }
+    }
+
+    prevBlock.TransferCmd = new ReturnCmd(Token.NoToken);
+    impl.Blocks = newBlocks;
+  }
+
+  public static void Predicate(Program p) {
+    foreach (var decl in p.TopLevelDeclarations) {
+      if (decl is DeclWithFormals && !(decl is Function)) {
+        var dwf = (DeclWithFormals)decl;
+        var fpVar = new LocalVariable(Token.NoToken,
+                                    new TypedIdent(Token.NoToken, "fp",
+                                                   Microsoft.Boogie.Type.Bool));
+        dwf.InParams = new VariableSeq((dwf.InParams + new VariableSeq(fpVar))
+                       .Cast<Variable>().ToArray());
+      }
+      var impl = decl as Implementation;
+      if (impl != null)
+        new BlockPredicator(p, impl).PredicateImplementation();
+    }
+  }
+
+}
+
+}
diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs
index 502844b2..7e6324b2 100644
--- a/Source/GPUVerify/CommandLineOptions.cs
+++ b/Source/GPUVerify/CommandLineOptions.cs
@@ -40,6 +40,8 @@ namespace GPUVerify
 

         public static bool NoLoopPredicateInvariants = false;

 

+        public static bool Unstructured = false;

+

         public static int Parse(string[] args)

         {

             for (int i = 0; i < args.Length; i++)

@@ -177,6 +179,11 @@ namespace GPUVerify
                     NoLoopPredicateInvariants = true;

                     break;

 

+                    case "-unstructured":

+                    case "/unstructured":

+                    Unstructured = true;

+                    break;

+

                     default:

                         inputFiles.Add(args[i]);

                         break;

@@ -216,6 +223,7 @@ namespace GPUVerify
   /divided         : check individual pairs of possibly racing statements separately

   /dividedArray    : check races on arrays one at a time

   /dividedElement  : ???

+  /unstructured    : operate on the unstructured form of the program

 

 ");

         }

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index f6ba390b..5d5bd4d6 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -102,19 +102,35 @@ namespace GPUVerify
 

         private Procedure CheckExactlyOneKernelProcedure()

         {

-            return CheckSingleInstanceOfAttributedProcedure(Program, "kernel");

+            var p = CheckSingleInstanceOfAttributedProcedure("kernel");

+            if (p == null)

+            {

+                Error(Program, "\"kernel\" attribute has not been specified for any procedure.  You must mark exactly one procedure with this attribute");

+            }

+

+            return p;

         }

 

-        private Procedure CheckExactlyOneBarrierProcedure()

+        private Procedure FindOrCreateBarrierProcedure()

         {

-            return CheckSingleInstanceOfAttributedProcedure(Program, "barrier");

+            var p = CheckSingleInstanceOfAttributedProcedure("barrier");

+            if (p == null)

+            {

+                p = new Procedure(Token.NoToken, "barrier", new TypeVariableSeq(),

+                                  new VariableSeq(), new VariableSeq(),

+                                  new RequiresSeq(), new IdentifierExprSeq(),

+                                  new EnsuresSeq(),

+                                  new QKeyValue(Token.NoToken, "barrier", new List<object>(), null));

+                Program.TopLevelDeclarations.Add(p);

+            }

+            return p;

         }

 

-        private Procedure CheckSingleInstanceOfAttributedProcedure(Program program, string attribute)

+        private Procedure CheckSingleInstanceOfAttributedProcedure(string attribute)

         {

             Procedure attributedProcedure = null;

 

-            foreach (Declaration decl in program.TopLevelDeclarations)

+            foreach (Declaration decl in Program.TopLevelDeclarations)

             {

                 if (!QKeyValue.FindBoolAttribute(decl.Attributes, attribute))

                 {

@@ -144,11 +160,6 @@ namespace GPUVerify
                 }

             }

 

-            if (attributedProcedure == null)

-            {

-                Error(program, "\"{0}\" attribute has not been specified for any procedure.  You must mark exactly one procedure with this attribute", attribute);

-            }

-

             return attributedProcedure;

         }

 

@@ -189,10 +200,20 @@ namespace GPUVerify
             return true;

         }

 

-        private bool FindNonLocalVariables(Program program)

+        private void MaybeCreateAttributedConst(string attr, ref Constant constFieldRef)

+        {

+            if (constFieldRef == null)

+            {

+                constFieldRef = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, attr, Microsoft.Boogie.Type.GetBvType(32)));

+                constFieldRef.AddAttribute(attr);

+                Program.TopLevelDeclarations.Add(constFieldRef);

+            }

+        }

+

+        private bool FindNonLocalVariables()

         {

             bool success = true;

-            foreach (Declaration D in program.TopLevelDeclarations)

+            foreach (Declaration D in Program.TopLevelDeclarations)

             {

                 if (D is Variable && (D as Variable).IsMutable)

                 {

@@ -232,6 +253,22 @@ namespace GPUVerify
                 }

             }

 

+            MaybeCreateAttributedConst(LOCAL_ID_X_STRING, ref _X);

+            MaybeCreateAttributedConst(LOCAL_ID_Y_STRING, ref _Y);

+            MaybeCreateAttributedConst(LOCAL_ID_Z_STRING, ref _Z);

+

+            MaybeCreateAttributedConst(GROUP_SIZE_X_STRING, ref _GROUP_SIZE_X);

+            MaybeCreateAttributedConst(GROUP_SIZE_Y_STRING, ref _GROUP_SIZE_Y);

+            MaybeCreateAttributedConst(GROUP_SIZE_Z_STRING, ref _GROUP_SIZE_Z);

+

+            MaybeCreateAttributedConst(GROUP_ID_X_STRING, ref _GROUP_X);

+            MaybeCreateAttributedConst(GROUP_ID_Y_STRING, ref _GROUP_Y);

+            MaybeCreateAttributedConst(GROUP_ID_Z_STRING, ref _GROUP_Z);

+

+            MaybeCreateAttributedConst(NUM_GROUPS_X_STRING, ref _NUM_GROUPS_X);

+            MaybeCreateAttributedConst(NUM_GROUPS_Y_STRING, ref _NUM_GROUPS_Y);

+            MaybeCreateAttributedConst(NUM_GROUPS_Z_STRING, ref _NUM_GROUPS_Z);

+

             return success;

         }

 

@@ -307,6 +344,10 @@ namespace GPUVerify
 

         internal void doit()

         {

+            if (CommandLineOptions.Unstructured)

+            {

+                Microsoft.Boogie.CommandLineOptions.Clo.PrintUnstructured = 2;

+            }

 

             if (CommandLineOptions.ShowStages)

             {

@@ -1920,7 +1961,7 @@ namespace GPUVerify
                 if (d is Implementation)

                 {

 

-                    new KernelDualiser(this).DualiseImplementation(d as Implementation);

+                    new KernelDualiser(this).DualiseImplementation(d as Implementation, CommandLineOptions.Unstructured);

 

                     NewTopLevelDeclarations.Add(d as Implementation);

 

@@ -1946,6 +1987,12 @@ namespace GPUVerify
 

         private void MakeKernelPredicated()

         {

+            if (CommandLineOptions.Unstructured)

+            {

+                BlockPredicator.Predicate(Program);

+                return;

+            }

+

             foreach (Declaration d in Program.TopLevelDeclarations)

             {

                 if (d is Procedure)

@@ -2007,7 +2054,7 @@ namespace GPUVerify
 

         private int Check()

         {

-            BarrierProcedure = CheckExactlyOneBarrierProcedure();

+            BarrierProcedure = FindOrCreateBarrierProcedure();

             KernelProcedure = CheckExactlyOneKernelProcedure();

 

             if (ErrorCount > 0)

@@ -2025,101 +2072,15 @@ namespace GPUVerify
                 Error(BarrierProcedure, "Barrier procedure must not return any results");

             }

 

-            if (!FindNonLocalVariables(Program))

+            if (!FindNonLocalVariables())

             {

                 return ErrorCount;

             }

 

             CheckKernelImplementation();

-

-            if (!KernelHasIdX())

-            {

-                MissingKernelAttributeError(LOCAL_ID_X_STRING);

-            }

-

-            if (!KernelHasGroupSizeX())

-            {

-                MissingKernelAttributeError(GROUP_SIZE_X_STRING);

-            }

-

-            if (!KernelHasNumGroupsX())

-            {

-                MissingKernelAttributeError(NUM_GROUPS_X_STRING);

-            }

-

-            if (!KernelHasGroupIdX())

-            {

-                MissingKernelAttributeError(GROUP_ID_X_STRING);

-            }

-

-            if (!KernelHasIdY())

-            {

-                MissingKernelAttributeError(LOCAL_ID_Y_STRING);

-            }

-

-            if (!KernelHasGroupSizeY())

-            {

-                MissingKernelAttributeError(GROUP_SIZE_Y_STRING);

-            }

-

-            if (!KernelHasNumGroupsY())

-            {

-                MissingKernelAttributeError(NUM_GROUPS_Y_STRING);

-            }

-

-            if (!KernelHasGroupIdY())

-            {

-                MissingKernelAttributeError(GROUP_ID_Y_STRING);

-            }

-

-            if (!KernelHasIdY())

-            {

-                MissingKernelAttributeError(LOCAL_ID_Y_STRING);

-            }

-

-            if (!KernelHasGroupSizeY())

-            {

-                MissingKernelAttributeError(GROUP_SIZE_Y_STRING);

-            }

-

-            if (!KernelHasNumGroupsY())

-            {

-                MissingKernelAttributeError(NUM_GROUPS_Y_STRING);

-            }

-

-            if (!KernelHasGroupIdY())

-            {

-                MissingKernelAttributeError(GROUP_ID_Y_STRING);

-            }

-

-            if (!KernelHasIdZ())

-            {

-                MissingKernelAttributeError(LOCAL_ID_Z_STRING);

-            }

-

-            if (!KernelHasGroupSizeZ())

-            {

-                MissingKernelAttributeError(GROUP_SIZE_Z_STRING);

-            }

-

-            if (!KernelHasNumGroupsZ())

-            {

-                MissingKernelAttributeError(NUM_GROUPS_Z_STRING);

-            }

-

-            if (!KernelHasGroupIdZ())

-            {

-                MissingKernelAttributeError(GROUP_ID_Z_STRING);

-            }

-

             return ErrorCount;

         }

 

-        private void MissingKernelAttributeError(string attribute)

-        {

-            Error(KernelProcedure.tok, "Kernel must declare global constant marked with attribute ':" + attribute + "'");

-        }

-

         public static bool IsThreadLocalIdConstant(Variable variable)

         {

             return variable.Name.Equals(_X.Name) || variable.Name.Equals(_Y.Name) || variable.Name.Equals(_Z.Name);

diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj
index b375efd9..27b9abe5 100644
--- a/Source/GPUVerify/GPUVerify.csproj
+++ b/Source/GPUVerify/GPUVerify.csproj
@@ -108,6 +108,8 @@
     <Compile Include="AccessRecord.cs" />

     <Compile Include="ArrayControlFlowAnalyser.cs" />

     <Compile Include="AsymmetricExpressionFinder.cs" />

+    <Compile Include="BlockPredicator.cs" />

+    <Compile Include="GraphAlgorithms.cs" />

     <Compile Include="InvariantGenerationRules\LoopVariableBoundsInvariantGenerator.cs" />

     <Compile Include="InvariantGenerationRules\InvariantGenerationRule.cs" />

     <Compile Include="InvariantGenerationRules\PowerOfTwoInvariantGenerator.cs" />

@@ -158,6 +160,10 @@
       <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>

       <Name>Core</Name>

     </ProjectReference>

+    <ProjectReference Include="..\Graph\Graph.csproj">

+      <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>

+      <Name>Graph</Name>

+    </ProjectReference>

     <ProjectReference Include="..\ParserHelper\ParserHelper.csproj">

       <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>

       <Name>ParserHelper</Name>

diff --git a/Source/GPUVerify/GraphAlgorithms.cs b/Source/GPUVerify/GraphAlgorithms.cs
new file mode 100644
index 00000000..3442a64d
--- /dev/null
+++ b/Source/GPUVerify/GraphAlgorithms.cs
@@ -0,0 +1,84 @@
+using Graphing;
+using System;
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using System.Linq;
+
+namespace GPUVerify {
+
+public static class GraphAlgorithms {
+
+  public static List<Tuple<Node, bool>> LoopyTopSort<Node>(this Graph<Node> g) {
+    Contract.Assert(g.Reducible);
+
+    int n = g.Nodes.Count;
+    var nodeToNumber = new Dictionary<Node, int>(n);
+    var numberToNode = new Node[n];
+    var allNodes = new List<int>();
+    int counter = 0;
+    foreach (Node node in g.Nodes) {
+      numberToNode[counter] = node;
+      nodeToNumber[node] = counter;
+      allNodes.Add(counter);
+      counter++;
+    }
+
+    var loops = new List<int>[n];
+    foreach (var h in g.Headers) {
+      var loopNodes = new HashSet<Node>();
+      foreach (var b in g.BackEdgeNodes(h))
+        loopNodes.UnionWith(g.NaturalLoops(h, b));
+      loops[nodeToNumber[h]] =
+        new List<int>(loopNodes.Select(node => nodeToNumber[node]));
+    }
+
+    var successors = new List<int>[n];
+    int[] incomingEdges = new int[n];
+
+    foreach (var e in g.Edges) {
+      Contract.Assert(e.Item1 != null);
+      Contract.Assert(e.Item2 != null);
+      int source = nodeToNumber[e.Item1], target = nodeToNumber[e.Item2];
+      if (loops[target] == null || !loops[target].Contains(source)) {
+        if (successors[source] == null)
+          successors[source] = new List<int>();
+        successors[source].Add(target);
+        incomingEdges[target]++;
+      }
+    }
+
+    var sortedNodes = new List<Tuple<Node, bool>>();
+
+    var regionStack = new Stack<Tuple<Node, List<int>>>();
+    regionStack.Push(new Tuple<Node, List<int>>(default(Node), allNodes));
+
+    while (regionStack.Count != 0) {
+      int rootIndex = -1;
+      foreach (var i in regionStack.Peek().Item2) {
+        if (incomingEdges[i] == 0) {
+          rootIndex = i;
+          break;
+        }
+      }
+      if (rootIndex == -1) {
+        var region = regionStack.Pop();
+        if (regionStack.Count != 0)
+          sortedNodes.Add(new Tuple<Node, bool>(region.Item1, true));
+        continue;
+      }
+      incomingEdges[rootIndex] = -1;
+      sortedNodes.Add(new Tuple<Node, bool>(numberToNode[rootIndex], false));
+      if (successors[rootIndex] != null)
+        foreach (int s in successors[rootIndex])
+          incomingEdges[s]--;
+      if (loops[rootIndex] != null)
+        regionStack.Push(new Tuple<Node, List<int>>(numberToNode[rootIndex],
+                                                    loops[rootIndex]));
+    }
+
+    return sortedNodes;
+  }
+
+}
+
+}
diff --git a/Source/GPUVerify/KernelDualiser.cs b/Source/GPUVerify/KernelDualiser.cs
index 0496a4e0..8d51e74e 100644
--- a/Source/GPUVerify/KernelDualiser.cs
+++ b/Source/GPUVerify/KernelDualiser.cs
@@ -82,145 +82,150 @@ namespace GPUVerify
             return result;

         }

 

-        private BigBlock MakeDual(BigBlock bb)

+        private void MakeDual(CmdSeq cs, Cmd c)

         {

-            // Not sure what to do about the transfer command

-

-            BigBlock result = new BigBlock(bb.tok, bb.LabelName, new CmdSeq(), null, bb.tc);

-

-            foreach (Cmd c in bb.simpleCmds)

+            if (c is CallCmd)

             {

-                if (c is CallCmd)

-                {

-                    CallCmd Call = c as CallCmd;

+                CallCmd Call = c as CallCmd;

 

-                    List<Expr> uniformNewIns = new List<Expr>();

-                    List<Expr> nonUniformNewIns = new List<Expr>();

-                    for (int i = 0; i < Call.Ins.Count; i++)

+                List<Expr> uniformNewIns = new List<Expr>();

+                List<Expr> nonUniformNewIns = new List<Expr>();

+                for (int i = 0; i < Call.Ins.Count; i++)

+                {

+                    if (verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetInParameter(Call.callee, i)))

                     {

-                        if (verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetInParameter(Call.callee, i)))

-                        {

-                            uniformNewIns.Add(Call.Ins[i]);

-                        }

-                        else

-                        {

-                            nonUniformNewIns.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(Call.Ins[i]));

-                        }

+                        uniformNewIns.Add(Call.Ins[i]);

                     }

-                    for (int i = 0; i < Call.Ins.Count; i++)

+                    else

                     {

-                        if (!(verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetInParameter(Call.callee, i))))

-                        {

-                            nonUniformNewIns.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(Call.Ins[i]));

-                        }

+                        nonUniformNewIns.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(Call.Ins[i]));

                     }

+                }

+                for (int i = 0; i < Call.Ins.Count; i++)

+                {

+                    if (!(verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetInParameter(Call.callee, i))))

+                    {

+                        nonUniformNewIns.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(Call.Ins[i]));

+                    }

+                }

 

-                    List<Expr> newIns = uniformNewIns;

-                    newIns.AddRange(nonUniformNewIns);

+                List<Expr> newIns = uniformNewIns;

+                newIns.AddRange(nonUniformNewIns);

 

-                    List<IdentifierExpr> uniformNewOuts = new List<IdentifierExpr>();

-                    List<IdentifierExpr> nonUniformNewOuts = new List<IdentifierExpr>();

-                    for (int i = 0; i < Call.Outs.Count; i++)

+                List<IdentifierExpr> uniformNewOuts = new List<IdentifierExpr>();

+                List<IdentifierExpr> nonUniformNewOuts = new List<IdentifierExpr>();

+                for (int i = 0; i < Call.Outs.Count; i++)

+                {

+                    if (verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetOutParameter(Call.callee, i)))

                     {

-                        if (verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetOutParameter(Call.callee, i)))

-                        {

-                            uniformNewOuts.Add(Call.Outs[i]);

-                        }

-                        else

-                        {

-                            nonUniformNewOuts.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(Call.Outs[i].Clone() as IdentifierExpr) as IdentifierExpr);

-                        }

-

+                        uniformNewOuts.Add(Call.Outs[i]);

                     }

-                    for (int i = 0; i < Call.Outs.Count; i++)

+                    else

                     {

-                        if (!(verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetOutParameter(Call.callee, i))))

-                        {

-                            nonUniformNewOuts.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(Call.Outs[i].Clone() as IdentifierExpr) as IdentifierExpr);

-                        }

+                        nonUniformNewOuts.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(Call.Outs[i].Clone() as IdentifierExpr) as IdentifierExpr);

                     }

 

-                    List<IdentifierExpr> newOuts = uniformNewOuts;

-                    newOuts.AddRange(nonUniformNewOuts);

-

-                    CallCmd NewCallCmd = new CallCmd(Call.tok, Call.callee, newIns, newOuts);

-

-                    NewCallCmd.Proc = Call.Proc;

-

-                    result.simpleCmds.Add(NewCallCmd);

                 }

-                else if (c is AssignCmd)

+                for (int i = 0; i < Call.Outs.Count; i++)

                 {

-                    AssignCmd assign = c as AssignCmd;

-

-                    Debug.Assert(assign.Lhss.Count == 1 && assign.Rhss.Count == 1);

-

-                    if (assign.Lhss[0] is SimpleAssignLhs &&

-                        verifier.uniformityAnalyser.IsUniform(procName, (assign.Lhss[0] as SimpleAssignLhs).AssignedVariable.Name))

+                    if (!(verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetOutParameter(Call.callee, i))))

                     {

-                        result.simpleCmds.Add(assign);

+                        nonUniformNewOuts.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(Call.Outs[i].Clone() as IdentifierExpr) as IdentifierExpr);

                     }

-                    else

-                    {

-                        List<AssignLhs> newLhss = new List<AssignLhs>();

-                        List<Expr> newRhss = new List<Expr>();

+                }

 

-                        newLhss.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).Visit(assign.Lhss.ElementAt(0).Clone() as AssignLhs) as AssignLhs);

-                        newLhss.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).Visit(assign.Lhss.ElementAt(0).Clone() as AssignLhs) as AssignLhs);

+                List<IdentifierExpr> newOuts = uniformNewOuts;

+                newOuts.AddRange(nonUniformNewOuts);

 

-                        newRhss.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(assign.Rhss.ElementAt(0).Clone() as Expr));

-                        newRhss.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(assign.Rhss.ElementAt(0).Clone() as Expr));

+                CallCmd NewCallCmd = new CallCmd(Call.tok, Call.callee, newIns, newOuts);

 

-                        AssignCmd newAssign = new AssignCmd(assign.tok, newLhss, newRhss);

+                NewCallCmd.Proc = Call.Proc;

 

-                        result.simpleCmds.Add(newAssign);

-                    }

+                cs.Add(NewCallCmd);

+            }

+            else if (c is AssignCmd)

+            {

+                AssignCmd assign = c as AssignCmd;

+

+                Debug.Assert(assign.Lhss.Count == 1 && assign.Rhss.Count == 1);

+

+                if (assign.Lhss[0] is SimpleAssignLhs &&

+                    verifier.uniformityAnalyser.IsUniform(procName, (assign.Lhss[0] as SimpleAssignLhs).AssignedVariable.Name))

+                {

+                    cs.Add(assign);

                 }

-                else if (c is HavocCmd)

+                else

                 {

-                    HavocCmd havoc = c as HavocCmd;

-                    Debug.Assert(havoc.Vars.Length == 1);

+                    List<AssignLhs> newLhss = new List<AssignLhs>();

+                    List<Expr> newRhss = new List<Expr>();

+

+                    newLhss.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).Visit(assign.Lhss.ElementAt(0).Clone() as AssignLhs) as AssignLhs);

+                    newLhss.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).Visit(assign.Lhss.ElementAt(0).Clone() as AssignLhs) as AssignLhs);

+

+                    newRhss.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(assign.Rhss.ElementAt(0).Clone() as Expr));

+                    newRhss.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(assign.Rhss.ElementAt(0).Clone() as Expr));

+

+                    AssignCmd newAssign = new AssignCmd(assign.tok, newLhss, newRhss);

+

+                    cs.Add(newAssign);

+                }

+            }

+            else if (c is HavocCmd)

+            {

+                HavocCmd havoc = c as HavocCmd;

+                Debug.Assert(havoc.Vars.Length == 1);

 

-                    HavocCmd newHavoc;

+                HavocCmd newHavoc;

 

-                    newHavoc = new HavocCmd(havoc.tok, new IdentifierExprSeq(new IdentifierExpr[] { 

-                        (IdentifierExpr)(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr)), 

-                        (IdentifierExpr)(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr))

-                    }));

+                newHavoc = new HavocCmd(havoc.tok, new IdentifierExprSeq(new IdentifierExpr[] { 

+                    (IdentifierExpr)(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr)), 

+                    (IdentifierExpr)(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr))

+                }));

 

-                    result.simpleCmds.Add(newHavoc);

+                cs.Add(newHavoc);

+            }

+            else if (c is AssertCmd)

+            {

+                AssertCmd ass = c as AssertCmd;

+                if (ContainsAsymmetricExpression(ass.Expr))

+                {

+                    cs.Add(new AssertCmd(c.tok, new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr)));

                 }

-                else if (c is AssertCmd)

+                else

                 {

-                    AssertCmd ass = c as AssertCmd;

-                    if (ContainsAsymmetricExpression(ass.Expr))

-                    {

-                        result.simpleCmds.Add(new AssertCmd(c.tok, new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr)));

-                    }

-                    else

-                    {

-                        result.simpleCmds.Add(new AssertCmd(c.tok, Expr.And(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr),

-                            new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr))));

-                    }

+                    cs.Add(new AssertCmd(c.tok, Expr.And(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr),

+                        new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr))));

                 }

-                else if (c is AssumeCmd)

+            }

+            else if (c is AssumeCmd)

+            {

+                AssumeCmd ass = c as AssumeCmd;

+                if (ContainsAsymmetricExpression(ass.Expr))

                 {

-                    AssumeCmd ass = c as AssumeCmd;

-                    if (ContainsAsymmetricExpression(ass.Expr))

-                    {

-                        result.simpleCmds.Add(new AssumeCmd(c.tok, new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr)));

-                    }

-                    else

-                    {

-                        result.simpleCmds.Add(new AssumeCmd(c.tok, Expr.And(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr),

-                            new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr))));

-                    }

+                    cs.Add(new AssumeCmd(c.tok, new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr)));

                 }

                 else

                 {

-                    Debug.Assert(false);

+                    cs.Add(new AssumeCmd(c.tok, Expr.And(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr),

+                        new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr))));

                 }

             }

+            else

+            {

+                Debug.Assert(false);

+            }

+        }

+

+        private BigBlock MakeDual(BigBlock bb)

+        {

+            // Not sure what to do about the transfer command

+

+            BigBlock result = new BigBlock(bb.tok, bb.LabelName, new CmdSeq(), null, bb.tc);

+

+            foreach (Cmd c in bb.simpleCmds)

+            {

+                MakeDual(result.simpleCmds, c);

+            }

 

             if (bb.ec is WhileCmd)

             {

@@ -262,6 +267,16 @@ namespace GPUVerify
 

         }

 

+        private Block MakeDual(Block b)

+        {

+            Block result = new Block(b.tok, b.Label, new CmdSeq(), b.TransferCmd);

+            foreach (Cmd c in b.Cmds)

+            {

+                MakeDual(result.Cmds, c);

+            }

+            return result;

+        }

+

         private List<PredicateCmd> MakeDualInvariants(List<PredicateCmd> originalInvariants)

         {

             List<PredicateCmd> result = new List<PredicateCmd>();

@@ -345,14 +360,17 @@ namespace GPUVerify
         }

 

 

-        internal void DualiseImplementation(Implementation impl)

+        internal void DualiseImplementation(Implementation impl, bool unstructured)

         {

             procName = impl.Name;

 

             impl.InParams = DualiseVariableSequence(impl.InParams);

             impl.OutParams = DualiseVariableSequence(impl.OutParams);

             MakeDualLocalVariables(impl);

-            impl.StructuredStmts = MakeDual(impl.StructuredStmts);

+            if (unstructured)

+                impl.Blocks = new List<Block>(impl.Blocks.Select(MakeDual));

+            else

+                impl.StructuredStmts = MakeDual(impl.StructuredStmts);

 

             procName = null;

         }

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 8f9f7498..e69c38b1 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -52,9 +52,7 @@ namespace VC
               Implementation impl = decl as Implementation;

               if (impl == null) continue;

               Contract.Assert(!impl.Name.StartsWith(recordProcName), "Not allowed to have an implementation for this guy");

-              if (impl.Proc.FindExprAttribute("inline") != null) {

-                implName2StratifiedInliningInfo[impl.Name] = new StratifiedInliningInfo(impl, this);

-              }

+              implName2StratifiedInliningInfo[impl.Name] = new StratifiedInliningInfo(impl, this);

             }

             this.GenerateRecordFunctions();

             PersistCallTree = false;

@@ -136,58 +134,63 @@ namespace VC
             return node;

           }

         }

-        

-        public class StratifiedVC {

-          private static int newVarCount = 0;

-          private static VCExprVar CreateNewVar(ProverInterface prover, Microsoft.Boogie.Type type) {

-            string newName = "StratifiedInlining@" + newVarCnt.ToString();

-            newVarCount++;

-            Constant newVar = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, type));

-            prover.Context.DeclareConstant(newVar, false, null);

-            return prover.VCExprGen.Variable(newVar.Name, type);

-          }

-          private static int idCount = 0;

 

+        private int newVarCount = 0;

+        public VCExprVar CreateNewVar(Microsoft.Boogie.Type type) {

+          string newName = "StratifiedInlining@" + newVarCnt.ToString();

+          newVarCount++;

+          Constant newVar = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, type));

+          prover.Context.DeclareConstant(newVar, false, null);

+          return prover.VCExprGen.Variable(newVar.Name, type);

+        }

+        private int idCount = 1; // 0 is reserved for the VC of main

+        public int CreateNewId() {

+          return idCount++;

+        }

+

+        public class StratifiedVC {

+          StratifiedInliningInfo info;

           int id;

-          Implementation impl;

           List<VCExprVar> interfaceExprVars;

           List<StratifiedCallSite> callSites;

           VCExpr vcexpr;

           public Dictionary<Block, VCExprVar> reachVars;

 

-          public StratifiedVC(StratifiedInliningInfo info, StratifiedVCGen vcgen) {

+          public StratifiedVC(StratifiedInliningInfo siInfo) {

+            info = siInfo;

             if (!info.initialized) {

-              info.GenerateVC(vcgen);

+              info.GenerateVC();

             }

 

-            impl = info.impl;

-            interfaceExprVars = new List<VCExprVar>();

             VCExpr expansion = info.vcexpr;

+            var vcgen = info.vcgen;

             var prover = vcgen.prover;

             VCExpressionGenerator gen = prover.VCExprGen;

             var bet = prover.Context.BoogieExprTranslator;

             VCExpr controlFlowVariableExpr = bet.LookupVariable(info.controlFlowVariable);

-            id = idCount++;

+            id = vcgen.CreateNewId();

             VCExpr eqExpr = gen.Eq(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(id)));

             expansion = gen.And(eqExpr, expansion);

 

+            interfaceExprVars = new List<VCExprVar>();

             Dictionary<VCExprVar, VCExpr> substDict = new Dictionary<VCExprVar, VCExpr>();

             foreach (VCExprVar v in info.interfaceExprVars) {

-              VCExprVar newVar = CreateNewVar(prover, v.Type);

+              VCExprVar newVar = vcgen.CreateNewVar(v.Type);

               interfaceExprVars.Add(newVar);

               substDict.Add(v, newVar);

             }

             foreach (VCExprVar v in info.privateExprVars) {

-              substDict.Add(v, CreateNewVar(prover, v.Type));

+              substDict.Add(v, vcgen.CreateNewVar(v.Type));

             }

             VCExprSubstitution subst = new VCExprSubstitution(substDict, new Dictionary<TypeVariable, Microsoft.Boogie.Type>());

             SubstitutingVCExprVisitor substVisitor = new SubstitutingVCExprVisitor(prover.VCExprGen);

             expansion = substVisitor.Mutate(expansion, subst);

-            

+

+            var impl = info.impl;

             reachVars = new Dictionary<Block, VCExprVar>();

             Dictionary<Block, VCExpr> reachExprs = new Dictionary<Block, VCExpr>();

             foreach (Block b in impl.Blocks) {

-              reachVars[b] = CreateNewVar(prover, Bpl.Type.Bool);

+              reachVars[b] = vcgen.CreateNewVar(Bpl.Type.Bool);

               reachExprs[b] = VCExpressionGenerator.False;

             }

             foreach (Block b in impl.Blocks) {

@@ -209,7 +212,16 @@ namespace VC
             foreach (CallSite cs in info.callSites) {

               callSites.Add(new StratifiedCallSite(cs, substVisitor, subst, reachVars));

             }

+          }

 

+          public VCExpr Attach(StratifiedCallSite stratifiedCallSite) {

+            Contract.Assert(interfaceExprVars.Count == stratifiedCallSite.interfaceExprVars.Count);

+            VCExpressionGenerator gen = info.vcgen.prover.VCExprGen;

+            VCExpr ret = gen.Eq(stratifiedCallSite.reachVar, reachVars[info.impl.Blocks[0]]);

+            for (int i = 0; i < stratifiedCallSite.interfaceExprVars.Count; i++) {

+              ret = gen.And(ret, gen.Eq(stratifiedCallSite.interfaceExprVars[i], interfaceExprVars[i]));

+            }

+            return ret;

           }

         }

 

@@ -225,9 +237,9 @@ namespace VC
         }

 

         public class StratifiedCallSite {

-          CallSite callSite;

-          List<VCExpr> interfaceExprVars;

-          VCExprVar reachVar;

+          public CallSite callSite;

+          public List<VCExpr> interfaceExprVars;

+          public VCExprVar reachVar;

 

           public StratifiedCallSite(CallSite cs, SubstitutingVCExprVisitor substVisitor, VCExprSubstitution subst, Dictionary<Block, VCExprVar> reachVars) {

             callSite = cs;

@@ -240,6 +252,7 @@ namespace VC
         }

 

         public class StratifiedInliningInfo {

+          public StratifiedVCGen vcgen;

           public Implementation impl;

           public Function function;

           public Variable controlFlowVariable;

@@ -252,7 +265,8 @@ namespace VC
           public List<CallSite> callSites;

           public bool initialized;

 

-          public StratifiedInliningInfo(Implementation implementation, StratifiedVCGen vcgen) {

+          public StratifiedInliningInfo(Implementation implementation, StratifiedVCGen stratifiedVcGen) {

+            vcgen = stratifiedVcGen;

             impl = implementation;

 

             VariableSeq functionInterfaceVars = new VariableSeq();

@@ -298,7 +312,7 @@ namespace VC
             initialized = false;

           }

 

-          public void GenerateVC(StratifiedVCGen vcgen) {

+          public void GenerateVC() {

             List<Variable> outputVariables = new List<Variable>();

             assertExpr = new LiteralExpr(Token.NoToken, true);

             foreach (Variable v in impl.OutParams) {

@@ -1054,7 +1068,7 @@ namespace VC
             public ApiChecker checker2;

 

             public VerificationState(VCExpr vcMain, FCallHandler calls, ProverInterface prover, ProverInterface.ErrorHandler reporter) {

-              prover.Assert(vcMain, false); 

+              prover.Assert(vcMain, true); 

               this.calls = calls;

               this.checker = new ApiChecker(prover, reporter);

               vcSize = 0;

@@ -1087,7 +1101,7 @@ namespace VC
             foreach (StratifiedInliningInfo info in implName2StratifiedInliningInfo.Values)

             {

                 Contract.Assert(info != null);

-                info.GenerateVC(this);

+                info.GenerateVC();

             }

 

             // Get the VC of the current procedure

@@ -1285,8 +1299,10 @@ namespace VC
 

         public override Outcome VerifyImplementation(Implementation/*!*/ impl, Program/*!*/ program, VerifierCallback/*!*/ callback)

         {

-            Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

+            if (!QKeyValue.FindBoolAttribute(impl.Attributes, "entrypoint")) 

+              return Outcome.Correct;

             Debug.Assert(this.program == program);

+

             var computeUnderBound = true;

 

             #region stratified inlining options

@@ -1320,11 +1336,12 @@ namespace VC
             }

 

             // Get the VC of the current procedure

-            VCExpr vc;

-            Hashtable/*<int, Absy!>*/ mainLabel2absy;

-            StratifiedInliningErrorReporter reporter;

-            GetVC(impl, program, prover, callback, out vc, out mainLabel2absy, out reporter);

-      

+            StratifiedInliningInfo info = implName2StratifiedInliningInfo[impl.Name];

+            info.GenerateVC();

+            VCExpr vc = info.vcexpr;

+            Hashtable mainLabel2absy = info.label2absy;

+            var reporter = new StratifiedInliningErrorReporter(implName2StratifiedInliningInfo, prover, callback, info.mvInfo, prover.Context, program, impl);

+

             // Find all procedure calls in vc and put labels on them      

             FCallHandler calls = new FCallHandler(prover.VCExprGen, implName2StratifiedInliningInfo, impl.Name, mainLabel2absy);

             calls.setCurrProcAsMain();

@@ -1773,7 +1790,7 @@ namespace VC
                 StratifiedInliningInfo info = implName2StratifiedInliningInfo[procName];

                 if (!info.initialized)

                 {

-                    info.GenerateVC(this);

+                    info.GenerateVC();

                 }

                 //Console.WriteLine("Inlining {0}", procName);

                 VCExpr expansion = cce.NonNull(info.vcexpr);

@@ -1883,7 +1900,7 @@ namespace VC
             }

 

             reporter = new StratifiedInliningErrorReporter(

-               cce.NonNull(implName2StratifiedInliningInfo), prover, callback, mvInfo, prover.Context, gotoCmdOrigins, program, impl);

+               cce.NonNull(implName2StratifiedInliningInfo), prover, callback, mvInfo, prover.Context, program, impl);

         }

 

 

@@ -2467,7 +2484,6 @@ namespace VC
             Program/*!*/ program;

             Implementation/*!*/ mainImpl;

             ProverContext/*!*/ context;

-            Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins;

 

             public bool underapproximationMode;

             public List<int>/*!*/ candidatesToExpand;

@@ -2487,7 +2503,6 @@ namespace VC
 

             public StratifiedInliningErrorReporter(Dictionary<string/*!*/, StratifiedInliningInfo/*!*/>/*!*/ implName2StratifiedInliningInfo,

                                                    ProverInterface/*!*/ theoremProver, VerifierCallback/*!*/ callback, ModelViewInfo mvInfo, ProverContext/*!*/ context,

-                                                   Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins,

                                                    Program/*!*/ program, Implementation/*!*/ mainImpl)

             {

                 Contract.Requires(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));

@@ -2505,7 +2520,6 @@ namespace VC
                 this.underapproximationMode = false;

                 this.calls = null;

                 this.candidatesToExpand = new List<int>();

-                this.gotoCmdOrigins = gotoCmdOrigins;

             }

 

             public void SetCandidateHandler(FCallHandler calls)

@@ -2637,21 +2651,14 @@ namespace VC
               Contract.Assert(CommandLineOptions.Clo.StratifiedInliningWithoutModels || model != null);

 

               candidatesToExpand = new List<int>();

+              var cex = GenerateTraceMain(labels, model, mvInfo);

 

-              if (underapproximationMode) {

-                var cex = GenerateTraceMain(labels, model, mvInfo);

+              if (underapproximationMode && cex != null) {

                 Debug.Assert(candidatesToExpand.All(calls.isSkipped));

-                if (cex != null) {

-                  GetModelWithStates(model);

-                  callback.OnCounterexample(cex, null);

-                  this.PrintModel(model);

-                }

-                return;

+                GetModelWithStates(model);

+                callback.OnCounterexample(cex, null);

+                this.PrintModel(model);

               }

-

-              Contract.Assert(calls != null);

-

-              GenerateTraceMain(labels, model, mvInfo);

             }

 

             // Construct the interprocedural trace

@@ -2663,28 +2670,7 @@ namespace VC
               }

 

               orderedStateIds = new List<Tuple<int, int>>();

-              Counterexample newCounterexample =

-               GenerateTrace(labels, errModel, 0, mainImpl);

-

-              if (newCounterexample == null)

-                return null;

-

-              #region Map passive program errors back to original program errors

-              ReturnCounterexample returnExample = newCounterexample as ReturnCounterexample;

-              if (returnExample != null && gotoCmdOrigins != null) {

-                foreach (Block b in returnExample.Trace) {

-                  Contract.Assert(b != null);

-                  Contract.Assume(b.TransferCmd != null);

-                  ReturnCmd cmd = (ReturnCmd)gotoCmdOrigins[b.TransferCmd];

-                  if (cmd != null) {

-                    returnExample.FailingReturn = cmd;

-                    break;

-                  }

-                }

-              }

-              #endregion

-

-              return newCounterexample;

+              return GenerateTrace(labels, errModel, 0, mainImpl);

             }

 

             private Counterexample GenerateTrace(IList<string/*!*/>/*!*/ labels, Model/*!*/ errModel,

diff --git a/Test/extractloops/Answer b/Test/extractloops/Answer
index bf30d427..08b1fffc 100644
--- a/Test/extractloops/Answer
+++ b/Test/extractloops/Answer
@@ -1,58 +1,58 @@
 ----- Running regression test t1.bpl

-t1.bpl(38,5): Error BP5001: This assertion might not hold.

+(0,0): Error BP5001: This assertion might not hold.

 Execution trace:

-    t1.bpl(19,3): anon0

-    t1.bpl(23,3): anon3_LoopHead

+    t1.bpl(17,3): anon0

+    t1.bpl(22,3): anon3_LoopHead

     Inlined call to procedure foo begins

-        t1.bpl(11,5): anon0

+        t1.bpl(8,5): anon0

     Inlined call to procedure foo ends

-    t1.bpl(27,3): anon3_LoopBody

-    t1.bpl(23,3): anon3_LoopHead

+    t1.bpl(26,3): anon3_LoopBody

+    t1.bpl(22,3): anon3_LoopHead

     Inlined call to procedure foo begins

-        t1.bpl(11,5): anon0

+        t1.bpl(8,5): anon0

     Inlined call to procedure foo ends

-    t1.bpl(27,3): anon3_LoopBody

-    t1.bpl(23,3): anon3_LoopHead

+    t1.bpl(26,3): anon3_LoopBody

+    t1.bpl(22,3): anon3_LoopHead

     Inlined call to procedure foo begins

-        t1.bpl(11,5): anon0

+        t1.bpl(8,5): anon0

     Inlined call to procedure foo ends

-    t1.bpl(33,3): anon3_LoopDone

-    t1.bpl(37,3): anon2

+    t1.bpl(32,3): anon3_LoopDone

+    t1.bpl(36,3): anon2

 

 Boogie program verifier finished with 0 verified, 1 error

 -----

 ----- Running regression test t2.bpl

-t2.bpl(51,5): Error BP5001: This assertion might not hold.

+(0,0): Error BP5001: This assertion might not hold.

 Execution trace:

-    t2.bpl(19,3): anon0

-    t2.bpl(23,3): anon3_LoopHead

+    t2.bpl(16,3): anon0

+    t2.bpl(21,3): anon3_LoopHead

     Inlined call to procedure foo begins

-        t2.bpl(11,5): anon0

+        t2.bpl(7,5): anon0

     Inlined call to procedure foo ends

-    t2.bpl(27,3): anon3_LoopBody

-    t2.bpl(34,3): lab1_LoopHead

-    t2.bpl(37,3): lab1_LoopBody

-    t2.bpl(34,3): lab1_LoopHead

-    t2.bpl(37,3): lab1_LoopBody

-    t2.bpl(34,3): lab1_LoopHead

-    t2.bpl(42,3): lab1_LoopDone

-    t2.bpl(23,3): anon3_LoopHead

+    t2.bpl(25,3): anon3_LoopBody

+    t2.bpl(32,3): lab1_LoopHead

+    t2.bpl(35,3): lab1_LoopBody

+    t2.bpl(32,3): lab1_LoopHead

+    t2.bpl(35,3): lab1_LoopBody

+    t2.bpl(32,3): lab1_LoopHead

+    t2.bpl(40,3): lab1_LoopDone

+    t2.bpl(21,3): anon3_LoopHead

     Inlined call to procedure foo begins

-        t2.bpl(11,5): anon0

+        t2.bpl(7,5): anon0

     Inlined call to procedure foo ends

-    t2.bpl(27,3): anon3_LoopBody

-    t2.bpl(34,3): lab1_LoopHead

-    t2.bpl(37,3): lab1_LoopBody

-    t2.bpl(34,3): lab1_LoopHead

-    t2.bpl(37,3): lab1_LoopBody

-    t2.bpl(34,3): lab1_LoopHead

-    t2.bpl(42,3): lab1_LoopDone

-    t2.bpl(23,3): anon3_LoopHead

+    t2.bpl(25,3): anon3_LoopBody

+    t2.bpl(32,3): lab1_LoopHead

+    t2.bpl(35,3): lab1_LoopBody

+    t2.bpl(32,3): lab1_LoopHead

+    t2.bpl(35,3): lab1_LoopBody

+    t2.bpl(32,3): lab1_LoopHead

+    t2.bpl(40,3): lab1_LoopDone

+    t2.bpl(21,3): anon3_LoopHead

     Inlined call to procedure foo begins

-        t2.bpl(11,5): anon0

+        t2.bpl(7,5): anon0

     Inlined call to procedure foo ends

-    t2.bpl(46,3): anon3_LoopDone

-    t2.bpl(50,3): anon2

+    t2.bpl(44,3): anon3_LoopDone

+    t2.bpl(48,3): anon2

 

 Boogie program verifier finished with 0 verified, 1 error

 -----

@@ -61,30 +61,25 @@ Boogie program verifier finished with 0 verified, 1 error
 Boogie program verifier finished with 1 verified, 0 errors

 -----

 ----- Running regression test t3.bpl with recursion bound 4

-t3.bpl(38,5): Error BP5001: This assertion might not hold.

+(0,0): Error BP5001: This assertion might not hold.

 Execution trace:

-    t3.bpl(19,3): anon0

-    t3.bpl(23,3): anon3_LoopHead

+    t3.bpl(15,3): anon0

+    t3.bpl(20,3): anon3_LoopHead

     Inlined call to procedure foo begins

-        t3.bpl(11,5): anon0

+        t3.bpl(6,5): anon0

     Inlined call to procedure foo ends

-    t3.bpl(27,3): anon3_LoopBody

-    t3.bpl(23,3): anon3_LoopHead

+    t3.bpl(24,3): anon3_LoopBody

+    t3.bpl(20,3): anon3_LoopHead

     Inlined call to procedure foo begins

-        t3.bpl(11,5): anon0

+        t3.bpl(6,5): anon0

     Inlined call to procedure foo ends

-    t3.bpl(27,3): anon3_LoopBody

-    t3.bpl(23,3): anon3_LoopHead

+    t3.bpl(24,3): anon3_LoopBody

+    t3.bpl(20,3): anon3_LoopHead

     Inlined call to procedure foo begins

-        t3.bpl(11,5): anon0

+        t3.bpl(6,5): anon0

     Inlined call to procedure foo ends

-    t3.bpl(33,3): anon3_LoopDone

-    t3.bpl(37,3): anon2

+    t3.bpl(30,3): anon3_LoopDone

+    t3.bpl(34,3): anon2

 

 Boogie program verifier finished with 0 verified, 1 error

 -----

------ Running regression test detLoopExtract.bpl with deterministicExtractLoops

-Stratified Inlining: Reached recursion bound of 4

-

-Boogie program verifier finished with 2 verified, 0 errors

------

diff --git a/Test/extractloops/t1.bpl b/Test/extractloops/t1.bpl
index 58b89e6b..00df45e9 100644
--- a/Test/extractloops/t1.bpl
+++ b/Test/extractloops/t1.bpl
@@ -1,22 +1,21 @@
 var g: int;

 

-procedure A();

-  requires g == 0;

-  modifies g;

 

-procedure {:inline 1} {:verify false} foo(); 

 

-implementation foo() {

+procedure foo()

+{

   var t: int;

   t := 0;

 }

 

-implementation A()

+procedure {:entrypoint} A()

+modifies g;

 {

   var x: int;

   var y: int;

 

   anon0:

+    assume g == 0;

     x := 4;

     goto anon3_LoopHead;

 

@@ -35,7 +34,7 @@ implementation A()
     goto anon2;

 

   anon2:

-    assert x == 1;

+    assume x != 1;

     return;

 }

 

diff --git a/Test/extractloops/t2.bpl b/Test/extractloops/t2.bpl
index d0011929..93f80f20 100644
--- a/Test/extractloops/t2.bpl
+++ b/Test/extractloops/t2.bpl
@@ -1,22 +1,20 @@
 var g: int;

 

-procedure A();

-  requires g == 0;

-  modifies g;

 

-procedure {:inline 1} {:verify false} foo(); 

-

-implementation foo() {

+procedure foo()

+{

   var t: int;

   t := 0;

 }

 

-implementation A()

+procedure {:entrypoint} A()

+modifies g;

 {

   var x: int;

   var y: int;

 

   anon0:

+    assume g == 0;

     x := 4;

     goto anon3_LoopHead;

 

@@ -48,8 +46,6 @@ implementation A()
     goto anon2;

 

   anon2:

-    assert false;

-    assert x == 1;

     return;

 }

 

diff --git a/Test/extractloops/t3.bpl b/Test/extractloops/t3.bpl
index e5fad6d1..d14767ab 100644
--- a/Test/extractloops/t3.bpl
+++ b/Test/extractloops/t3.bpl
@@ -1,22 +1,19 @@
 var g: int;

 

-procedure A();

-  requires g == 0;

-  modifies g;

-

-procedure {:inline 1} {:verify false} foo(); 

-

-implementation foo() {

+procedure foo()

+{

   var t: int;

   t := 0;

 }

 

-implementation A()

+procedure {:entrypoint} A()

+modifies g;

 {

   var x: int;

   var y: int;

 

   anon0:

+    assume g == 0;

     x := 4;

     goto anon3_LoopHead, anon3_LoopBody;

 

@@ -35,7 +32,7 @@ implementation A()
     goto anon2;

 

   anon2:

-    assert x == 1;

+    assume x != 1;

     return;

 }

 

diff --git a/Test/stratifiedinline/Answer b/Test/stratifiedinline/Answer
index 77b00b19..dd5344e8 100644
--- a/Test/stratifiedinline/Answer
+++ b/Test/stratifiedinline/Answer
@@ -1,8 +1,7 @@
 ----- Running regression test bar1.bpl

-bar1.bpl(25,1): Error BP5003: A postcondition might not hold on this return path.

-bar1.bpl(21,1): Related location: This is the postcondition that might not hold.

+(0,0): Error BP5001: This assertion might not hold.

 Execution trace:

-    bar1.bpl(24,3): anon0

+    bar1.bpl(22,3): anon0

     Inlined call to procedure foo begins

         bar1.bpl(13,5): anon0

         Inlined call to procedure bar begins

@@ -16,25 +15,24 @@ Execution trace:
 Boogie program verifier finished with 0 verified, 1 error

 -----

 ----- Running regression test bar2.bpl

-bar2.bpl(21,3): Error BP5001: This assertion might not hold.

+(0,0): Error BP5001: This assertion might not hold.

 Execution trace:

-    bar2.bpl(19,3): anon0

+    bar2.bpl(18,3): anon0

     Inlined call to procedure foo begins

-        bar2.bpl(5,3): anon0

-        bar2.bpl(9,7): anon3_Else

+        bar2.bpl(4,3): anon0

+        bar2.bpl(5,7): anon3_Then

     Inlined call to procedure foo ends

     Inlined call to procedure foo begins

-        bar2.bpl(5,3): anon0

-        bar2.bpl(6,7): anon3_Then

+        bar2.bpl(4,3): anon0

+        bar2.bpl(8,7): anon3_Else

     Inlined call to procedure foo ends

 

 Boogie program verifier finished with 0 verified, 1 error

 -----

 ----- Running regression test bar3.bpl

-bar3.bpl(41,1): Error BP5003: A postcondition might not hold on this return path.

-bar3.bpl(34,1): Related location: This is the postcondition that might not hold.

+(0,0): Error BP5001: This assertion might not hold.

 Execution trace:

-    bar3.bpl(38,3): anon0

+    bar3.bpl(35,3): anon0

     Inlined call to procedure foo begins

         bar3.bpl(18,3): anon0

         bar3.bpl(19,7): anon3_Then

@@ -63,7 +61,7 @@ Boogie program verifier finished with 1 verified, 0 errors
 Boogie program verifier finished with 1 verified, 0 errors

 -----

 ----- Running regression test bar7.bpl

-bar7.bpl(42,3): Error BP5001: This assertion might not hold.

+(0,0): Error BP5001: This assertion might not hold.

 Execution trace:

     bar7.bpl(35,5): anon0

     bar7.bpl(37,5): anon4_Then

@@ -156,7 +154,7 @@ Execution trace:
 Boogie program verifier finished with 0 verified, 1 error

 -----

 ----- Running regression test bar8.bpl

-bar8.bpl(41,3): Error BP5001: This assertion might not hold.

+(0,0): Error BP5001: This assertion might not hold.

 Execution trace:

     bar8.bpl(34,5): anon0

     bar8.bpl(36,5): anon4_Then

@@ -249,7 +247,7 @@ Execution trace:
 Boogie program verifier finished with 0 verified, 1 error

 -----

 ----- Running regression test bar9.bpl

-bar9.bpl(44,3): Error BP5001: This assertion might not hold.

+(0,0): Error BP5001: This assertion might not hold.

 Execution trace:

     bar9.bpl(35,5): anon0

     bar9.bpl(41,5): anon4_Else

@@ -386,7 +384,7 @@ Execution trace:
 Boogie program verifier finished with 0 verified, 1 error

 -----

 ----- Running regression test bar10.bpl

-bar10.bpl(40,3): Error BP5001: This assertion might not hold.

+(0,0): Error BP5001: This assertion might not hold.

 Execution trace:

     bar10.bpl(35,5): anon0

     Inlined call to procedure bar1 begins

@@ -485,10 +483,9 @@ Execution trace:
 Boogie program verifier finished with 0 verified, 1 error

 -----

 ----- Running regression test bar11.bpl

-bar11.bpl(31,1): Error BP5003: A postcondition might not hold on this return path.

-bar11.bpl(26,1): Related location: This is the postcondition that might not hold.

+(0,0): Error BP5001: This assertion might not hold.

 Execution trace:

-    bar11.bpl(30,3): anon0

+    bar11.bpl(26,3): anon0

     Inlined call to procedure foo begins

         bar11.bpl(15,3): anon0

         value = 0

diff --git a/Test/stratifiedinline/bar1.bpl b/Test/stratifiedinline/bar1.bpl
index 845954d5..bd210f70 100644
--- a/Test/stratifiedinline/bar1.bpl
+++ b/Test/stratifiedinline/bar1.bpl
@@ -1,13 +1,13 @@
 var x: int;

 var y: int;

 

-procedure {:inline 1} bar()

+procedure bar()

 modifies y;

 {

   y := y + 1;

 }

 

-procedure {:inline 1} foo() 

+procedure foo() 

 modifies x, y;

 {

   x := x + 1;

@@ -16,11 +16,11 @@ modifies x, y;
   x := x + 1;

 }

 

-procedure main()

-requires x == y;

-ensures x != y;

+procedure {:entrypoint} main()

 modifies x, y;

 {

+  assume x == y;

   call foo();

+  assume x == y;

 }

 

diff --git a/Test/stratifiedinline/bar10.bpl b/Test/stratifiedinline/bar10.bpl
index 8cfcfc13..ab1e4748 100644
--- a/Test/stratifiedinline/bar10.bpl
+++ b/Test/stratifiedinline/bar10.bpl
@@ -1,7 +1,7 @@
 var i: int;

 var m: int;

 

-procedure {:inline 1} foo()

+procedure foo()

 modifies i;

 {

   if (i < 20) {

@@ -10,7 +10,7 @@ modifies i;
   }

 }

 

-procedure {:inline 1} bar1(j: int) 

+procedure bar1(j: int) 

 modifies i;

 {

   if (j < 2*m) 

@@ -20,7 +20,7 @@ modifies i;
   }

 }

 

-procedure {:inline 1} bar2(j: int) 

+procedure bar2(j: int) 

 modifies i;

 {

   if (j < m) {

@@ -29,7 +29,7 @@ modifies i;
   }

 }

 

-procedure main() 

+procedure {:entrypoint} main() 

 modifies i;

 {

   i := 0;

@@ -37,5 +37,5 @@ modifies i;
   call bar2(0);

   i := 0;

   call foo();

-  assert i < 10;

+  assume !(i < 10);

 }
\ No newline at end of file
diff --git a/Test/stratifiedinline/bar11.bpl b/Test/stratifiedinline/bar11.bpl
index baad27a1..67e21ba6 100644
--- a/Test/stratifiedinline/bar11.bpl
+++ b/Test/stratifiedinline/bar11.bpl
@@ -2,14 +2,14 @@ var x: int;
 var y: int;

 procedure boogie_si_record_int(x:int);

 

-procedure {:inline 1} bar()

+procedure bar()

 modifies y;

 {

   y := y + 1;

   call boogie_si_record_int(y);

 }

 

-procedure {:inline 1} foo() 

+procedure foo() 

 modifies x, y;

 {

   call boogie_si_record_int(x);

@@ -20,13 +20,12 @@ modifies x, y;
   call boogie_si_record_int(x);

 }

 

-procedure main()

-requires x == 0;

-requires x == y;

-ensures x != y;

+procedure {:entrypoint} main()

 modifies x, y;

 {

-

+  assume x == 0;

+  assume x == y;

   call foo();

+  assume x == y;

 }

 

diff --git a/Test/stratifiedinline/bar2.bpl b/Test/stratifiedinline/bar2.bpl
index 76991a8f..6c383591 100644
--- a/Test/stratifiedinline/bar2.bpl
+++ b/Test/stratifiedinline/bar2.bpl
@@ -1,5 +1,4 @@
-

-procedure {:inline 1} foo() returns (x: bool)

+procedure foo() returns (x: bool)

 {

   var b: bool;

   if (b) {

@@ -11,14 +10,14 @@ procedure {:inline 1} foo() returns (x: bool)
   }

 }

 

-procedure main()

+procedure {:entrypoint} main()

 {

   var b1: bool;

   var b2: bool;

 

   call b1 := foo();

   call b2 := foo();

-  assert b1 == b2;

+  assume b1 != b2;

 }

 

 

diff --git a/Test/stratifiedinline/bar3.bpl b/Test/stratifiedinline/bar3.bpl
index 7bd91184..a1f0bea3 100644
--- a/Test/stratifiedinline/bar3.bpl
+++ b/Test/stratifiedinline/bar3.bpl
@@ -1,7 +1,7 @@
 var y: int;

 var x: int;

 

-procedure {:inline 1} bar(b: bool)

+procedure bar(b: bool)

 modifies y;

 {

   if (b) {

@@ -11,7 +11,7 @@ modifies y;
   }

 }

 

-procedure {:inline 1} foo() 

+procedure foo() 

 modifies x, y;

 {

   var b: bool;

@@ -29,13 +29,11 @@ modifies x, y;
 }

 

 

-procedure main()

-requires x == y;

-ensures x == y;

+procedure {:entrypoint} main()

 modifies x, y;

-modifies y;

 {

+  assume x == y;

   call foo();

-  assert x == y;

   call bar(false);

+  assume x != y;

 }

diff --git a/Test/stratifiedinline/bar4.bpl b/Test/stratifiedinline/bar4.bpl
index 84640811..4b3a6ee2 100644
--- a/Test/stratifiedinline/bar4.bpl
+++ b/Test/stratifiedinline/bar4.bpl
@@ -1,7 +1,7 @@
 var y: int;

 var x: int;

 

-procedure {:inline 1} bar() returns (b: bool)

+procedure bar() returns (b: bool)

 modifies y;

 {

   if (b) {

@@ -11,7 +11,7 @@ modifies y;
   }

 }

 

-procedure {:inline 1} foo() 

+procedure foo() 

 modifies x, y;

 {

   var b: bool;

@@ -25,14 +25,13 @@ modifies x, y;
 }

 

 

-procedure main() returns (b: bool)

-requires x == y;

-ensures !b ==> x == y+1;

-ensures b ==> x+1 == y;

+procedure {:entrypoint} main() returns (b: bool)

 modifies x, y;

-modifies y;

 {

+  assume x == y;

   call foo();

-  assert x == y;

-  call b := bar();

+  if (x == y) {

+    call b := bar();

+    assume (if b then x+1 != y else x != y+1);

+  }

 }

diff --git a/Test/stratifiedinline/bar6.bpl b/Test/stratifiedinline/bar6.bpl
index e133aef7..dd528f6f 100644
--- a/Test/stratifiedinline/bar6.bpl
+++ b/Test/stratifiedinline/bar6.bpl
@@ -1,6 +1,6 @@
 var M: [int]int;

 

-procedure {:inline 1} bar(y: int) returns (b: bool)

+procedure bar(y: int) returns (b: bool)

 modifies M;

 {

   if (b) {

@@ -10,7 +10,7 @@ modifies M;
   }

 }

 

-procedure {:inline 1} foo(x: int, y: int) 

+procedure foo(x: int, y: int) 

 modifies M;

 {

   var b: bool;

@@ -23,14 +23,14 @@ modifies M;
   }

 }

 

-procedure main(x: int, y: int) returns (b: bool)

-requires x != y;

-requires M[x] == M[y];

-ensures !b ==> M[x] == M[y]+1;

-ensures b ==> M[x]+1 == M[y];

+procedure {:entrypoint} main(x: int, y: int) returns (b: bool)

 modifies M;

 {

+  assume x != y;

+  assume M[x] == M[y];

   call foo(x, y);

-  assert M[x] == M[y];

-  call b := bar(y);

+  if (M[x] == M[y]) {

+    call b := bar(y);

+    assume (if b then M[x]+1 != M[y] else M[x] != M[y]+1);

+  }

 }

diff --git a/Test/stratifiedinline/bar7.bpl b/Test/stratifiedinline/bar7.bpl
index b28777bd..41cf612e 100644
--- a/Test/stratifiedinline/bar7.bpl
+++ b/Test/stratifiedinline/bar7.bpl
@@ -1,7 +1,7 @@
 var i: int;

 var m: int;

 

-procedure {:inline 1} foo()

+procedure foo()

 modifies i;

 {

   if (i < 20) {

@@ -10,7 +10,7 @@ modifies i;
   }

 }

 

-procedure {:inline 1} bar1(j: int) 

+procedure bar1(j: int) 

 modifies i;

 {

   if (j < 2*m) 

@@ -20,7 +20,7 @@ modifies i;
   }

 }

 

-procedure {:inline 1} bar2(j: int) 

+procedure bar2(j: int) 

 modifies i;

 {

   if (j < m) {

@@ -29,7 +29,7 @@ modifies i;
   }

 }

 

-procedure main() 

+procedure {:entrypoint} main() 

 modifies i;

 {

   i := 0;

@@ -39,5 +39,5 @@ modifies i;
     call bar1(0);

     call bar2(0);

   }

-  assert i < 10;

+  assume !(i < 10);

 }
\ No newline at end of file
diff --git a/Test/stratifiedinline/bar8.bpl b/Test/stratifiedinline/bar8.bpl
index e96655f3..356645e6 100644
--- a/Test/stratifiedinline/bar8.bpl
+++ b/Test/stratifiedinline/bar8.bpl
@@ -1,7 +1,7 @@
 var i: int;

 var m: int;

 

-procedure {:inline 1} foo() 

+procedure foo() 

 modifies i;

 {

   if (i < 20) {

@@ -10,7 +10,7 @@ modifies i;
   }

 }

 

-procedure {:inline 1} bar1(j: int) 

+procedure bar1(j: int) 

 modifies i;

 {

   if (j < 2*m) {

@@ -19,7 +19,7 @@ modifies i;
   }

 }

 

-procedure {:inline 1} bar2(j: int) 

+procedure bar2(j: int) 

 modifies i;

 {

   if (j < m) {

@@ -28,7 +28,7 @@ modifies i;
   }

 }

 

-procedure main()

+procedure {:entrypoint} main()

 modifies i;

 {

   i := 0;

@@ -38,5 +38,5 @@ modifies i;
     call bar1(0);

     call bar2(0);

   }

-  assert i < 10;

+  assume !(i < 10);

 }
\ No newline at end of file
diff --git a/Test/stratifiedinline/bar9.bpl b/Test/stratifiedinline/bar9.bpl
index 12de78ad..d1eacb18 100644
--- a/Test/stratifiedinline/bar9.bpl
+++ b/Test/stratifiedinline/bar9.bpl
@@ -1,7 +1,7 @@
 var i: int;

 var m: int;

 

-procedure {:inline 1} foo(x: int)

+procedure foo(x: int)

 modifies i;

 {

   if (i < x) {

@@ -10,7 +10,7 @@ modifies i;
   }

 }

 

-procedure {:inline 1} bar1(j: int) 

+procedure bar1(j: int) 

 modifies i;

 {

   if (j < 2*m) 

@@ -20,7 +20,7 @@ modifies i;
   }

 }

 

-procedure {:inline 1} bar2(j: int) 

+procedure bar2(j: int) 

 modifies i;

 {

   if (j < m) {

@@ -29,7 +29,7 @@ modifies i;
   }

 }

 

-procedure main() 

+procedure {:entrypoint} main() 

 modifies i;

 {

   i := 0;

@@ -41,5 +41,5 @@ modifies i;
     call bar1(0);

     call bar2(0);

   }

-  assert i < 10;

+  assume !(i < 10);

 }
\ No newline at end of file
diff --git a/_admin/Chalice/aste/summary.log b/_admin/Chalice/aste/summary.log
index e676ecd8..ade80273 100644
--- a/_admin/Chalice/aste/summary.log
+++ b/_admin/Chalice/aste/summary.log
@@ -1,9 +1,9 @@
-# Aste started: 2012-05-22 09:04:38

+# Aste started: 2012-05-25 09:05:16

 # Host id: Boogiebox

 # Configuration: chalice.cfg

 # Task: aste.tasks.chalice.FullBuild

-# [2012-05-22 09:05:24] Chalice revision: 5b532a1a7343

-[2012-05-22 09:06:48] cmd /c "(set JAVA_OPTS=-Dsbt.ivy.home=D:\temp\.ivy2\) && (sbt.bat clean compile)"

+# [2012-05-25 09:06:05] Chalice revision: 8d9c6d63a543

+[2012-05-25 09:07:29] cmd /c "(set JAVA_OPTS=-Dsbt.ivy.home=D:\temp\.ivy2\) && (sbt.bat clean compile)"

 

     [warn] D:\temp\aste\Boogie\Chalice\src\main\scala\Ast.scala:77: case class `class SeqClass' has case class ancestor `class Class'.  This has been deprecated for unduly complicating both usage and implementation.  You should instead use extractors for pattern matching on non-leaf nodes.


     [warn] D:\temp\aste\Boogie\Chalice\src\main\scala\Ast.scala:111: case class `class TokenClass' has case class ancestor `class Class'.  This has been deprecated for unduly complicating both usage and implementation.  You should instead use extractors for pattern matching on non-leaf nodes.


@@ -11,6 +11,5 @@
     [warn] D:\temp\aste\Boogie\Chalice\src\main\scala\Ast.scala:141: case class `class TokenType' has case class ancestor `class Type'.  This has been deprecated for unduly complicating both usage and implementation.  You should instead use extractors for pattern matching on non-leaf nodes.


     [warn] D:\temp\aste\Boogie\Chalice\src\main\scala\Ast.scala:168: case class `class SpecialField' has case class ancestor `class Field'.  This has been deprecated for unduly complicating both usage and implementation.  You should instead use extractors for pattern matching on non-leaf nodes.


     [warn] D:\temp\aste\Boogie\Chalice\src\main\scala\Ast.scala:227: case class `class SpecialVariable' has case class ancestor `class Variable'.  This has been deprecated for unduly complicating both usage and implementation.  You should instead use extractors for pattern matching on non-leaf nodes.


-[2012-05-22 10:22:41] 1 out of 83 test(s) failed

-['list-reverse.chalice\r']

-# [2012-05-22 10:23:44] Released nightly of Chalice

+[2012-05-25 10:22:31] 0 out of 83 test(s) failed

+# [2012-05-25 10:23:12] Released nightly of Chalice