summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Source/Concurrency/CivlRefinement.cs2
-rw-r--r--Source/Concurrency/CivlTypeChecker.cs20
-rw-r--r--Source/Concurrency/YieldTypeChecker.cs2
-rw-r--r--Test/civl/DeviceCache.bpl.expect2
-rw-r--r--Test/civl/FlanaganQadeer.bpl.expect2
-rw-r--r--Test/civl/Program1.bpl.expect2
-rw-r--r--Test/civl/Program2.bpl.expect2
-rw-r--r--Test/civl/Program3.bpl.expect2
-rw-r--r--Test/civl/Program4.bpl.expect2
-rw-r--r--Test/civl/Program5.bpl.expect2
-rw-r--r--Test/civl/StoreBuffer.bpl.expect2
-rw-r--r--Test/civl/akash.bpl.expect2
-rw-r--r--Test/civl/alloc.bpl.expect2
-rw-r--r--Test/civl/bar.bpl.expect2
-rw-r--r--Test/civl/chris2.bpl.expect2
-rw-r--r--Test/civl/chris6.bpl14
-rw-r--r--Test/civl/chris6.bpl.expect5
-rw-r--r--Test/civl/civl-paper.bpl.expect2
-rw-r--r--Test/civl/foo.bpl.expect2
-rw-r--r--Test/civl/ghost.bpl.expect2
-rw-r--r--Test/civl/linear-set.bpl.expect2
-rw-r--r--Test/civl/linear-set2.bpl.expect2
-rw-r--r--Test/civl/lock-introduced.bpl.expect2
-rw-r--r--Test/civl/lock.bpl.expect2
-rw-r--r--Test/civl/lock2.bpl.expect2
-rw-r--r--Test/civl/multiset.bpl.expect2
-rw-r--r--Test/civl/new1.bpl.expect2
-rw-r--r--Test/civl/one.bpl.expect2
-rw-r--r--Test/civl/par-incr.bpl.expect2
-rw-r--r--Test/civl/parallel1.bpl.expect2
-rw-r--r--Test/civl/parallel2.bpl.expect2
-rw-r--r--Test/civl/parallel4.bpl.expect2
-rw-r--r--Test/civl/parallel5.bpl.expect2
-rw-r--r--Test/civl/perm.bpl.expect2
-rw-r--r--Test/civl/t1.bpl.expect2
-rw-r--r--Test/civl/termination2.bpl.expect2
-rw-r--r--Test/civl/ticket.bpl.expect2
-rw-r--r--Test/civl/treiber-stack.bpl.expect2
-rw-r--r--Test/civl/wsq.bpl.expect2
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