another fix requested by Chris

verification is performed now for all created layers

39 files changed, 55 insertions, 56 deletions

diff --git a/Source/Concurrency/CivlRefinement.cs b/Source/Concurrency/CivlRefinement.cs
index 43d0f60c..8fc27be9 100644
--- a/Source/Concurrency/CivlRefinement.cs
+++ b/Source/Concurrency/CivlRefinement.cs
@@ -1212,7 +1212,7 @@ namespace Microsoft.Boogie
         public static void AddCheckers(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, List<Declaration> decls)
         {
             Program program = linearTypeChecker.program;
-            foreach (int layerNum in civlTypeChecker.AllImplementedLayerNums)
+            foreach (int layerNum in civlTypeChecker.AllCreatedLayerNums)
             {
                 if (CommandLineOptions.Clo.TrustLayersDownto <= layerNum || layerNum <= CommandLineOptions.Clo.TrustLayersUpto) continue;
 
diff --git a/Source/Concurrency/CivlTypeChecker.cs b/Source/Concurrency/CivlTypeChecker.cs
index dba7ab4b..5215bc52 100644
--- a/Source/Concurrency/CivlTypeChecker.cs
+++ b/Source/Concurrency/CivlTypeChecker.cs
@@ -486,26 +486,6 @@ namespace Microsoft.Boogie
             }
         }
 
-        private HashSet<int> allImplementedLayerNums;
-        public IEnumerable<int> AllImplementedLayerNums
-        {
-            get
-            {
-                if (allImplementedLayerNums == null)
-                {
-                    allImplementedLayerNums = new HashSet<int>();
-                    foreach (ActionInfo actionInfo in procToActionInfo.Values)
-                    {
-                        if (actionInfo.hasImplementation)
-                        {
-                            allImplementedLayerNums.Add(actionInfo.createdAtLayerNum);
-                        }
-                    }
-                }
-                return allImplementedLayerNums;
-            }
-        }
-
         private HashSet<int> allCreatedLayerNums;
         public IEnumerable<int> AllCreatedLayerNums
         {
diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs
index a69f066d..027e7e83 100644
--- a/Source/Concurrency/YieldTypeChecker.cs
+++ b/Source/Concurrency/YieldTypeChecker.cs
@@ -141,7 +141,7 @@ namespace Microsoft.Boogie
                 Graph<Block> implGraph = Program.GraphFromImpl(impl);
                 implGraph.ComputeLoops();
                 int specLayerNum = civlTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum;
-                foreach (int layerNum in civlTypeChecker.AllImplementedLayerNums)
+                foreach (int layerNum in civlTypeChecker.AllCreatedLayerNums)
                 {
                     if (layerNum > specLayerNum) continue;
                     YieldTypeChecker executor = new YieldTypeChecker(civlTypeChecker, impl, layerNum, implGraph.Headers);
diff --git a/Test/civl/DeviceCache.bpl.expect b/Test/civl/DeviceCache.bpl.expect
index c4cf5ccf..129e60e2 100644
--- a/Test/civl/DeviceCache.bpl.expect
+++ b/Test/civl/DeviceCache.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 30 verified, 0 errors
+Boogie program verifier finished with 39 verified, 0 errors
diff --git a/Test/civl/FlanaganQadeer.bpl.expect b/Test/civl/FlanaganQadeer.bpl.expect
index 00ddb38b..76a9a2bf 100644
--- a/Test/civl/FlanaganQadeer.bpl.expect
+++ b/Test/civl/FlanaganQadeer.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 4 verified, 0 errors
+Boogie program verifier finished with 8 verified, 0 errors
diff --git a/Test/civl/Program1.bpl.expect b/Test/civl/Program1.bpl.expect
index 41374b00..00ddb38b 100644
--- a/Test/civl/Program1.bpl.expect
+++ b/Test/civl/Program1.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 2 verified, 0 errors
+Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/civl/Program2.bpl.expect b/Test/civl/Program2.bpl.expect
index a9949f2e..9823d44a 100644
--- a/Test/civl/Program2.bpl.expect
+++ b/Test/civl/Program2.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 3 verified, 0 errors
+Boogie program verifier finished with 6 verified, 0 errors
diff --git a/Test/civl/Program3.bpl.expect b/Test/civl/Program3.bpl.expect
index a9949f2e..9823d44a 100644
--- a/Test/civl/Program3.bpl.expect
+++ b/Test/civl/Program3.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 3 verified, 0 errors
+Boogie program verifier finished with 6 verified, 0 errors
diff --git a/Test/civl/Program4.bpl.expect b/Test/civl/Program4.bpl.expect
index a9949f2e..9823d44a 100644
--- a/Test/civl/Program4.bpl.expect
+++ b/Test/civl/Program4.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 3 verified, 0 errors
+Boogie program verifier finished with 6 verified, 0 errors
diff --git a/Test/civl/Program5.bpl.expect b/Test/civl/Program5.bpl.expect
index fde7e712..4bcb1071 100644
--- a/Test/civl/Program5.bpl.expect
+++ b/Test/civl/Program5.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 18 verified, 0 errors
+Boogie program verifier finished with 21 verified, 0 errors
diff --git a/Test/civl/StoreBuffer.bpl.expect b/Test/civl/StoreBuffer.bpl.expect
index 8c74fe2e..1931ffd2 100644
--- a/Test/civl/StoreBuffer.bpl.expect
+++ b/Test/civl/StoreBuffer.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 17 verified, 0 errors
+Boogie program verifier finished with 27 verified, 0 errors
diff --git a/Test/civl/akash.bpl.expect b/Test/civl/akash.bpl.expect
index 00ddb38b..76a9a2bf 100644
--- a/Test/civl/akash.bpl.expect
+++ b/Test/civl/akash.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 4 verified, 0 errors
+Boogie program verifier finished with 8 verified, 0 errors
diff --git a/Test/civl/alloc.bpl.expect b/Test/civl/alloc.bpl.expect
index f08c6e00..4bcb1071 100644
--- a/Test/civl/alloc.bpl.expect
+++ b/Test/civl/alloc.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 12 verified, 0 errors
+Boogie program verifier finished with 21 verified, 0 errors
diff --git a/Test/civl/bar.bpl.expect b/Test/civl/bar.bpl.expect
index 810c93bf..be6722fe 100644
--- a/Test/civl/bar.bpl.expect
+++ b/Test/civl/bar.bpl.expect
@@ -10,4 +10,4 @@ Execution trace:
     (0,0): anon00
     (0,0): inline$Impl_YieldChecker_PC_1$0$L0
 
-Boogie program verifier finished with 3 verified, 2 errors
+Boogie program verifier finished with 8 verified, 2 errors
diff --git a/Test/civl/chris2.bpl.expect b/Test/civl/chris2.bpl.expect
index ddb8537e..f3b66f4a 100644
--- a/Test/civl/chris2.bpl.expect
+++ b/Test/civl/chris2.bpl.expect
@@ -15,4 +15,4 @@ Execution trace:
 Execution trace:
     (0,0): this_A
 
-Boogie program verifier finished with 1 verified, 4 errors
+Boogie program verifier finished with 2 verified, 4 errors
diff --git a/Test/civl/chris6.bpl b/Test/civl/chris6.bpl
new file mode 100644
index 00000000..a0aecf1e
--- /dev/null
+++ b/Test/civl/chris6.bpl
@@ -0,0 +1,14 @@
+// RUN: %boogie -noinfer -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure{:extern}{:yields}{:layer 1,2} P1();
+  requires{:layer 1} false;
+  ensures{:atomic} |{ A: return true; }|;
+
+procedure{:yields}{:layer 2,3} P2()
+  ensures{:atomic} |{ A: return true; }|;
+{
+  assert{:layer 1} false;
+  yield;
+  call P1();
+  yield;
+}
diff --git a/Test/civl/chris6.bpl.expect b/Test/civl/chris6.bpl.expect
new file mode 100644
index 00000000..229e4e10
--- /dev/null
+++ b/Test/civl/chris6.bpl.expect
@@ -0,0 +1,5 @@
+chris6.bpl(10,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    chris6.bpl(10,3): anon0
+
+Boogie program verifier finished with 1 verified, 1 error
diff --git a/Test/civl/civl-paper.bpl.expect b/Test/civl/civl-paper.bpl.expect
index 11d204a8..bd1df2f9 100644
--- a/Test/civl/civl-paper.bpl.expect
+++ b/Test/civl/civl-paper.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 35 verified, 0 errors
+Boogie program verifier finished with 45 verified, 0 errors
diff --git a/Test/civl/foo.bpl.expect b/Test/civl/foo.bpl.expect
index 41e30691..44a93860 100644
--- a/Test/civl/foo.bpl.expect
+++ b/Test/civl/foo.bpl.expect
@@ -5,4 +5,4 @@ Execution trace:
     foo.bpl(14,3): inline$Incr_1$0$A
     (0,0): inline$Impl_YieldChecker_PC_1$0$L0
 
-Boogie program verifier finished with 4 verified, 1 error
+Boogie program verifier finished with 9 verified, 1 error
diff --git a/Test/civl/ghost.bpl.expect b/Test/civl/ghost.bpl.expect
index 9823d44a..76a9a2bf 100644
--- a/Test/civl/ghost.bpl.expect
+++ b/Test/civl/ghost.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 6 verified, 0 errors
+Boogie program verifier finished with 8 verified, 0 errors
diff --git a/Test/civl/linear-set.bpl.expect b/Test/civl/linear-set.bpl.expect
index 00ddb38b..76a9a2bf 100644
--- a/Test/civl/linear-set.bpl.expect
+++ b/Test/civl/linear-set.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 4 verified, 0 errors
+Boogie program verifier finished with 8 verified, 0 errors
diff --git a/Test/civl/linear-set2.bpl.expect b/Test/civl/linear-set2.bpl.expect
index 00ddb38b..76a9a2bf 100644
--- a/Test/civl/linear-set2.bpl.expect
+++ b/Test/civl/linear-set2.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 4 verified, 0 errors
+Boogie program verifier finished with 8 verified, 0 errors
diff --git a/Test/civl/lock-introduced.bpl.expect b/Test/civl/lock-introduced.bpl.expect
index f08c6e00..8c74fe2e 100644
--- a/Test/civl/lock-introduced.bpl.expect
+++ b/Test/civl/lock-introduced.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 12 verified, 0 errors
+Boogie program verifier finished with 17 verified, 0 errors
diff --git a/Test/civl/lock.bpl.expect b/Test/civl/lock.bpl.expect
index 3e6d423a..76a9a2bf 100644
--- a/Test/civl/lock.bpl.expect
+++ b/Test/civl/lock.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 5 verified, 0 errors
+Boogie program verifier finished with 8 verified, 0 errors
diff --git a/Test/civl/lock2.bpl.expect b/Test/civl/lock2.bpl.expect
index 3e6d423a..76a9a2bf 100644
--- a/Test/civl/lock2.bpl.expect
+++ b/Test/civl/lock2.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 5 verified, 0 errors
+Boogie program verifier finished with 8 verified, 0 errors
diff --git a/Test/civl/multiset.bpl.expect b/Test/civl/multiset.bpl.expect
index 0a77c517..63682bb4 100644
--- a/Test/civl/multiset.bpl.expect
+++ b/Test/civl/multiset.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 78 verified, 0 errors
+Boogie program verifier finished with 85 verified, 0 errors
diff --git a/Test/civl/new1.bpl.expect b/Test/civl/new1.bpl.expect
index 41374b00..00ddb38b 100644
--- a/Test/civl/new1.bpl.expect
+++ b/Test/civl/new1.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 2 verified, 0 errors
+Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/civl/one.bpl.expect b/Test/civl/one.bpl.expect
index 37fad75c..41374b00 100644
--- a/Test/civl/one.bpl.expect
+++ b/Test/civl/one.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 1 verified, 0 errors
+Boogie program verifier finished with 2 verified, 0 errors
diff --git a/Test/civl/par-incr.bpl.expect b/Test/civl/par-incr.bpl.expect
index 00ddb38b..3e3dc54b 100644
--- a/Test/civl/par-incr.bpl.expect
+++ b/Test/civl/par-incr.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 4 verified, 0 errors
+Boogie program verifier finished with 7 verified, 0 errors
diff --git a/Test/civl/parallel1.bpl.expect b/Test/civl/parallel1.bpl.expect
index 889ee4f2..fa974099 100644
--- a/Test/civl/parallel1.bpl.expect
+++ b/Test/civl/parallel1.bpl.expect
@@ -5,4 +5,4 @@ Execution trace:
     parallel1.bpl(14,3): inline$Incr_1$0$A
     (0,0): inline$Impl_YieldChecker_PC_1$0$L0
 
-Boogie program verifier finished with 3 verified, 1 error
+Boogie program verifier finished with 7 verified, 1 error
diff --git a/Test/civl/parallel2.bpl.expect b/Test/civl/parallel2.bpl.expect
index 3e6d423a..12041afe 100644
--- a/Test/civl/parallel2.bpl.expect
+++ b/Test/civl/parallel2.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 5 verified, 0 errors
+Boogie program verifier finished with 10 verified, 0 errors
diff --git a/Test/civl/parallel4.bpl.expect b/Test/civl/parallel4.bpl.expect
index 2d4c8148..baf228c8 100644
--- a/Test/civl/parallel4.bpl.expect
+++ b/Test/civl/parallel4.bpl.expect
@@ -3,4 +3,4 @@ Execution trace:
     parallel4.bpl(29,5): anon0
     (0,0): anon01
 
-Boogie program verifier finished with 3 verified, 1 error
+Boogie program verifier finished with 7 verified, 1 error
diff --git a/Test/civl/parallel5.bpl.expect b/Test/civl/parallel5.bpl.expect
index 3e6d423a..12041afe 100644
--- a/Test/civl/parallel5.bpl.expect
+++ b/Test/civl/parallel5.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 5 verified, 0 errors
+Boogie program verifier finished with 10 verified, 0 errors
diff --git a/Test/civl/perm.bpl.expect b/Test/civl/perm.bpl.expect
index 41374b00..00ddb38b 100644
--- a/Test/civl/perm.bpl.expect
+++ b/Test/civl/perm.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 2 verified, 0 errors
+Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/civl/t1.bpl.expect b/Test/civl/t1.bpl.expect
index fcef7e58..27a208d4 100644
--- a/Test/civl/t1.bpl.expect
+++ b/Test/civl/t1.bpl.expect
@@ -6,4 +6,4 @@ Execution trace:
     t1.bpl(25,21): inline$SetG_1$0$A
     (0,0): inline$Impl_YieldChecker_A_1$0$L1
 
-Boogie program verifier finished with 4 verified, 1 error
+Boogie program verifier finished with 9 verified, 1 error
diff --git a/Test/civl/termination2.bpl.expect b/Test/civl/termination2.bpl.expect
index 37fad75c..41374b00 100644
--- a/Test/civl/termination2.bpl.expect
+++ b/Test/civl/termination2.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 1 verified, 0 errors
+Boogie program verifier finished with 2 verified, 0 errors
diff --git a/Test/civl/ticket.bpl.expect b/Test/civl/ticket.bpl.expect
index b072912b..dc45a0ee 100644
--- a/Test/civl/ticket.bpl.expect
+++ b/Test/civl/ticket.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 16 verified, 0 errors
+Boogie program verifier finished with 24 verified, 0 errors
diff --git a/Test/civl/treiber-stack.bpl.expect b/Test/civl/treiber-stack.bpl.expect
index 9823d44a..76a9a2bf 100644
--- a/Test/civl/treiber-stack.bpl.expect
+++ b/Test/civl/treiber-stack.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 6 verified, 0 errors
+Boogie program verifier finished with 8 verified, 0 errors
diff --git a/Test/civl/wsq.bpl.expect b/Test/civl/wsq.bpl.expect
index a9949f2e..9823d44a 100644
--- a/Test/civl/wsq.bpl.expect
+++ b/Test/civl/wsq.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 3 verified, 0 errors
+Boogie program verifier finished with 6 verified, 0 errors