From 70fe7a30835aaeeda4f545afdad4a63ace5032c8 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 7 May 2014 19:54:44 +0100 Subject: Enabled bitvector lit tests. --- Test/bitvectors/Answer | 32 ++++++++++++++++---------------- Test/bitvectors/arrays.bpl | 2 ++ Test/bitvectors/arrays.bpl.expect | 2 ++ Test/bitvectors/bv0.bpl | 2 ++ Test/bitvectors/bv0.bpl.expect | 8 ++++++++ Test/bitvectors/bv1.bpl | 2 ++ Test/bitvectors/bv1.bpl.expect | 2 ++ Test/bitvectors/bv10.bpl | 2 ++ Test/bitvectors/bv10.bpl.expect | 2 ++ Test/bitvectors/bv2.bpl | 2 ++ Test/bitvectors/bv2.bpl.expect | 4 ++++ Test/bitvectors/bv3.bpl | 2 ++ Test/bitvectors/bv3.bpl.expect | 2 ++ Test/bitvectors/bv4.bpl | 2 ++ Test/bitvectors/bv4.bpl.expect | 2 ++ Test/bitvectors/bv5.bpl | 2 ++ Test/bitvectors/bv5.bpl.expect | 5 +++++ Test/bitvectors/bv6.bpl | 4 +++- Test/bitvectors/bv6.bpl.expect | 5 +++++ Test/bitvectors/bv7.bpl | 2 ++ Test/bitvectors/bv7.bpl.expect | 3 +++ Test/bitvectors/bv8.bpl | 2 ++ Test/bitvectors/bv8.bpl.expect | 2 ++ Test/bitvectors/bv9.bpl | 2 ++ Test/bitvectors/bv9.bpl.expect | 2 ++ 25 files changed, 80 insertions(+), 17 deletions(-) create mode 100644 Test/bitvectors/arrays.bpl.expect create mode 100644 Test/bitvectors/bv0.bpl.expect create mode 100644 Test/bitvectors/bv1.bpl.expect create mode 100644 Test/bitvectors/bv10.bpl.expect create mode 100644 Test/bitvectors/bv2.bpl.expect create mode 100644 Test/bitvectors/bv3.bpl.expect create mode 100644 Test/bitvectors/bv4.bpl.expect create mode 100644 Test/bitvectors/bv5.bpl.expect create mode 100644 Test/bitvectors/bv6.bpl.expect create mode 100644 Test/bitvectors/bv7.bpl.expect create mode 100644 Test/bitvectors/bv8.bpl.expect create mode 100644 Test/bitvectors/bv9.bpl.expect (limited to 'Test/bitvectors') diff --git a/Test/bitvectors/Answer b/Test/bitvectors/Answer index e20474d9..6aa2bce2 100644 --- a/Test/bitvectors/Answer +++ b/Test/bitvectors/Answer @@ -2,42 +2,42 @@ Boogie program verifier finished with 2 verified, 0 errors -------------------- bv0.bpl -------------------- -bv0.bpl(4,3): Error: mismatched types in assignment command (cannot assign bv31 to bv32) -bv0.bpl(5,3): Error: mismatched types in assignment command (cannot assign int to bv32) -bv0.bpl(6,4): Error: mismatched types in assignment command (cannot assign bv1 to bv32) -bv0.bpl(7,10): Error: start index in extract must be no bigger than the end index +bv0.bpl(6,3): Error: mismatched types in assignment command (cannot assign bv31 to bv32) +bv0.bpl(7,3): Error: mismatched types in assignment command (cannot assign int to bv32) bv0.bpl(8,4): Error: mismatched types in assignment command (cannot assign bv1 to bv32) -bv0.bpl(9,4): Error: mismatched types in assignment command (cannot assign bv1 to bv32) -bv0.bpl(10,4): Error: mismatched types in assignment command (cannot assign concat$bvproxy#10 to bv32) +bv0.bpl(9,10): Error: start index in extract must be no bigger than the end index +bv0.bpl(10,4): Error: mismatched types in assignment command (cannot assign bv1 to bv32) +bv0.bpl(11,4): Error: mismatched types in assignment command (cannot assign bv1 to bv32) +bv0.bpl(12,4): Error: mismatched types in assignment command (cannot assign concat$bvproxy#10 to bv32) 7 type checking errors detected in bv0.bpl -------------------- bv1.bpl -------------------- Boogie program verifier finished with 1 verified, 0 errors -------------------- bv2.bpl -------------------- -bv2.bpl(4,13): Error: bitvector bounds in illegal position -bv2.bpl(6,13): Error: undeclared type: x -bv2.bpl(7,14): Error: bitvector bounds in illegal position +bv2.bpl(6,13): Error: bitvector bounds in illegal position +bv2.bpl(8,13): Error: undeclared type: x +bv2.bpl(9,14): Error: bitvector bounds in illegal position 3 name resolution errors detected in bv2.bpl -------------------- bv3.bpl -------------------- -bv3.bpl(2,5): Error: type name: bv16 is registered for bitvectors +bv3.bpl(4,5): Error: type name: bv16 is registered for bitvectors 1 name resolution errors detected in bv3.bpl -------------------- bv4.bpl -------------------- Boogie program verifier finished with 1 verified, 0 errors -------------------- bv7.bpl -------------------- -bv7.bpl(4,14): error: arguments of extract need to be integer literals -bv7.bpl(5,15): error: parentheses around bitvector bounds are not allowed +bv7.bpl(6,14): error: arguments of extract need to be integer literals +bv7.bpl(7,15): error: parentheses around bitvector bounds are not allowed 2 parse errors detected in bv7.bpl -------------------- bv5.bpl -------------------- -bv5.bpl(10,3): Error BP5001: This assertion might not hold. +bv5.bpl(12,3): Error BP5001: This assertion might not hold. Execution trace: - bv5.bpl(5,12): anon0 + bv5.bpl(7,12): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- bv6.bpl -------------------- -bv6.bpl(8,3): Error BP5001: This assertion might not hold. +bv6.bpl(10,3): Error BP5001: This assertion might not hold. Execution trace: - bv6.bpl(5,5): anon0 + bv6.bpl(7,5): anon0 Boogie program verifier finished with 0 verified, 1 error -------------------- bv8.bpl -------------------- diff --git a/Test/bitvectors/arrays.bpl b/Test/bitvectors/arrays.bpl index dc304d27..17fc64a1 100644 --- a/Test/bitvectors/arrays.bpl +++ b/Test/bitvectors/arrays.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -proverWarnings:1 %s > %t +// RUN: %diff %s.expect %t const unique f1 : Field int; const unique f2 : Field bv32; const unique f3 : Field bool; diff --git a/Test/bitvectors/arrays.bpl.expect b/Test/bitvectors/arrays.bpl.expect new file mode 100644 index 00000000..41374b00 --- /dev/null +++ b/Test/bitvectors/arrays.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 2 verified, 0 errors diff --git a/Test/bitvectors/bv0.bpl b/Test/bitvectors/bv0.bpl index 43bf734a..18c6f5b8 100644 --- a/Test/bitvectors/bv0.bpl +++ b/Test/bitvectors/bv0.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -proverWarnings:1 %s > %t +// RUN: %diff %s.expect %t procedure foo2(x : bv32) returns(r : bv32) { block1: diff --git a/Test/bitvectors/bv0.bpl.expect b/Test/bitvectors/bv0.bpl.expect new file mode 100644 index 00000000..c5e2349c --- /dev/null +++ b/Test/bitvectors/bv0.bpl.expect @@ -0,0 +1,8 @@ +bv0.bpl(6,3): Error: mismatched types in assignment command (cannot assign bv31 to bv32) +bv0.bpl(7,3): Error: mismatched types in assignment command (cannot assign int to bv32) +bv0.bpl(8,4): Error: mismatched types in assignment command (cannot assign bv1 to bv32) +bv0.bpl(9,10): Error: start index in extract must be no bigger than the end index +bv0.bpl(10,4): Error: mismatched types in assignment command (cannot assign bv1 to bv32) +bv0.bpl(11,4): Error: mismatched types in assignment command (cannot assign bv1 to bv32) +bv0.bpl(12,4): Error: mismatched types in assignment command (cannot assign concat$bvproxy#10 to bv32) +7 type checking errors detected in bv0.bpl diff --git a/Test/bitvectors/bv1.bpl b/Test/bitvectors/bv1.bpl index 6c9ea70b..50c33cc3 100644 --- a/Test/bitvectors/bv1.bpl +++ b/Test/bitvectors/bv1.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -proverWarnings:1 %s > %t +// RUN: %diff %s.expect %t procedure foo(x : bv32) returns(r : bv32) { var q : bv64; diff --git a/Test/bitvectors/bv1.bpl.expect b/Test/bitvectors/bv1.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/bitvectors/bv1.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/bitvectors/bv10.bpl b/Test/bitvectors/bv10.bpl index 7c325d95..99ee6f86 100644 --- a/Test/bitvectors/bv10.bpl +++ b/Test/bitvectors/bv10.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie %s > %t +// RUN: %diff %s.expect %t var x: bv32; procedure main() diff --git a/Test/bitvectors/bv10.bpl.expect b/Test/bitvectors/bv10.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/bitvectors/bv10.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/bitvectors/bv2.bpl b/Test/bitvectors/bv2.bpl index f1888c2b..633c24e8 100644 --- a/Test/bitvectors/bv2.bpl +++ b/Test/bitvectors/bv2.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -proverWarnings:1 %s > %t +// RUN: %diff %s.expect %t procedure foo2(x : bv32) returns(r : bv32) { block1: diff --git a/Test/bitvectors/bv2.bpl.expect b/Test/bitvectors/bv2.bpl.expect new file mode 100644 index 00000000..14533ad1 --- /dev/null +++ b/Test/bitvectors/bv2.bpl.expect @@ -0,0 +1,4 @@ +bv2.bpl(6,13): Error: bitvector bounds in illegal position +bv2.bpl(8,13): Error: undeclared type: x +bv2.bpl(9,14): Error: bitvector bounds in illegal position +3 name resolution errors detected in bv2.bpl diff --git a/Test/bitvectors/bv3.bpl b/Test/bitvectors/bv3.bpl index 93e06077..3c2d1034 100644 --- a/Test/bitvectors/bv3.bpl +++ b/Test/bitvectors/bv3.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -proverWarnings:1 %s > %t +// RUN: %diff %s.expect %t type bv; type bv16; diff --git a/Test/bitvectors/bv3.bpl.expect b/Test/bitvectors/bv3.bpl.expect new file mode 100644 index 00000000..7ad8bc35 --- /dev/null +++ b/Test/bitvectors/bv3.bpl.expect @@ -0,0 +1,2 @@ +bv3.bpl(4,5): Error: type name: bv16 is registered for bitvectors +1 name resolution errors detected in bv3.bpl diff --git a/Test/bitvectors/bv4.bpl b/Test/bitvectors/bv4.bpl index f38891ff..71bc9fd1 100644 --- a/Test/bitvectors/bv4.bpl +++ b/Test/bitvectors/bv4.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -proverWarnings:1 %s > %t +// RUN: %diff %s.expect %t function a() returns(bv32); axiom a() == a(); diff --git a/Test/bitvectors/bv4.bpl.expect b/Test/bitvectors/bv4.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/bitvectors/bv4.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/bitvectors/bv5.bpl b/Test/bitvectors/bv5.bpl index f9240e1c..48683f32 100644 --- a/Test/bitvectors/bv5.bpl +++ b/Test/bitvectors/bv5.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie %s > %t +// RUN: %diff %s.expect %t procedure P() returns () { var m : [a]int; diff --git a/Test/bitvectors/bv5.bpl.expect b/Test/bitvectors/bv5.bpl.expect new file mode 100644 index 00000000..ebc7d335 --- /dev/null +++ b/Test/bitvectors/bv5.bpl.expect @@ -0,0 +1,5 @@ +bv5.bpl(12,3): Error BP5001: This assertion might not hold. +Execution trace: + bv5.bpl(7,12): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/bitvectors/bv6.bpl b/Test/bitvectors/bv6.bpl index ca8f8367..7e943888 100644 --- a/Test/bitvectors/bv6.bpl +++ b/Test/bitvectors/bv6.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie %s > %t +// RUN: %diff %s.expect %t procedure Q() returns () { var x : bv32, y : bv16; @@ -6,4 +8,4 @@ procedure Q() returns () { assert x[16:0] == y; assert x == x[16:0] ++ y; assert x[17:1] == y; // should not be verifiable -} \ No newline at end of file +} diff --git a/Test/bitvectors/bv6.bpl.expect b/Test/bitvectors/bv6.bpl.expect new file mode 100644 index 00000000..8948a8ba --- /dev/null +++ b/Test/bitvectors/bv6.bpl.expect @@ -0,0 +1,5 @@ +bv6.bpl(10,3): Error BP5001: This assertion might not hold. +Execution trace: + bv6.bpl(7,5): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/bitvectors/bv7.bpl b/Test/bitvectors/bv7.bpl index 2302cf2f..77069bd8 100644 --- a/Test/bitvectors/bv7.bpl +++ b/Test/bitvectors/bv7.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -proverWarnings:1 %s > %t +// RUN: %diff %s.expect %t procedure foo2(x : bv32) returns(r : bv32) { block1: diff --git a/Test/bitvectors/bv7.bpl.expect b/Test/bitvectors/bv7.bpl.expect new file mode 100644 index 00000000..223c162a --- /dev/null +++ b/Test/bitvectors/bv7.bpl.expect @@ -0,0 +1,3 @@ +bv7.bpl(6,14): error: arguments of extract need to be integer literals +bv7.bpl(7,15): error: parentheses around bitvector bounds are not allowed +2 parse errors detected in bv7.bpl diff --git a/Test/bitvectors/bv8.bpl b/Test/bitvectors/bv8.bpl index 7295f684..bd50bc89 100644 --- a/Test/bitvectors/bv8.bpl +++ b/Test/bitvectors/bv8.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie %s > %t +// RUN: %diff %s.expect %t // This file includes some tests for which Boogie once generated bad Z3 input procedure foo() diff --git a/Test/bitvectors/bv8.bpl.expect b/Test/bitvectors/bv8.bpl.expect new file mode 100644 index 00000000..41374b00 --- /dev/null +++ b/Test/bitvectors/bv8.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 2 verified, 0 errors diff --git a/Test/bitvectors/bv9.bpl b/Test/bitvectors/bv9.bpl index 9637c87f..96275528 100644 --- a/Test/bitvectors/bv9.bpl +++ b/Test/bitvectors/bv9.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -proverOpt:OPTIMIZE_FOR_BV=true %s > %t +// RUN: %diff %s.expect %t procedure foo(); implementation foo() diff --git a/Test/bitvectors/bv9.bpl.expect b/Test/bitvectors/bv9.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/bitvectors/bv9.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors -- cgit v1.2.3