Enabled bitvector lit tests.

25 files changed, 80 insertions, 17 deletions

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>[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