From c1b06a908ab1ed746672dd42eaf9417916a297cc Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Thu, 1 Oct 2015 09:40:42 -0700 Subject: another fix requested by Chris verification is performed now for all created layers --- Test/civl/DeviceCache.bpl.expect | 2 +- Test/civl/FlanaganQadeer.bpl.expect | 2 +- Test/civl/Program1.bpl.expect | 2 +- Test/civl/Program2.bpl.expect | 2 +- Test/civl/Program3.bpl.expect | 2 +- Test/civl/Program4.bpl.expect | 2 +- Test/civl/Program5.bpl.expect | 2 +- Test/civl/StoreBuffer.bpl.expect | 2 +- Test/civl/akash.bpl.expect | 2 +- Test/civl/alloc.bpl.expect | 2 +- Test/civl/bar.bpl.expect | 2 +- Test/civl/chris2.bpl.expect | 2 +- Test/civl/chris6.bpl | 14 ++++++++++++++ Test/civl/chris6.bpl.expect | 5 +++++ Test/civl/civl-paper.bpl.expect | 2 +- Test/civl/foo.bpl.expect | 2 +- Test/civl/ghost.bpl.expect | 2 +- Test/civl/linear-set.bpl.expect | 2 +- Test/civl/linear-set2.bpl.expect | 2 +- Test/civl/lock-introduced.bpl.expect | 2 +- Test/civl/lock.bpl.expect | 2 +- Test/civl/lock2.bpl.expect | 2 +- Test/civl/multiset.bpl.expect | 2 +- Test/civl/new1.bpl.expect | 2 +- Test/civl/one.bpl.expect | 2 +- Test/civl/par-incr.bpl.expect | 2 +- Test/civl/parallel1.bpl.expect | 2 +- Test/civl/parallel2.bpl.expect | 2 +- Test/civl/parallel4.bpl.expect | 2 +- Test/civl/parallel5.bpl.expect | 2 +- Test/civl/perm.bpl.expect | 2 +- Test/civl/t1.bpl.expect | 2 +- Test/civl/termination2.bpl.expect | 2 +- Test/civl/ticket.bpl.expect | 2 +- Test/civl/treiber-stack.bpl.expect | 2 +- Test/civl/wsq.bpl.expect | 2 +- 36 files changed, 53 insertions(+), 34 deletions(-) create mode 100644 Test/civl/chris6.bpl create mode 100644 Test/civl/chris6.bpl.expect (limited to 'Test') 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 -- cgit v1.2.3