diff options
| author |  Dan Liew <daniel.liew@imperial.ac.uk> | 2014-05-07 20:20:50 +0100 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-05-07 20:20:50 +0100 |
| commit | 6e432c44193931690a8992df2713a160e7548531 (patch) | |
| tree | 74bff526a0ee05c9bfc75e7ba49b107923a7957a | |
| parent | d9ed5e32fd306f0da3fc2a24ec17c81bff1c24fc (diff) | |
Enabled datatypes lit tests.
| -rw-r--r-- | Test/datatypes/Answer | 8 | ||||
| -rw-r--r-- | Test/datatypes/ex.bpl | 2 | ||||
| -rw-r--r-- | Test/datatypes/ex.bpl.expect | 2 | ||||
| -rw-r--r-- | Test/datatypes/t1.bpl | 2 | ||||
| -rw-r--r-- | Test/datatypes/t1.bpl.expect | 5 | ||||
| -rw-r--r-- | Test/datatypes/t2.bpl | 2 | ||||
| -rw-r--r-- | Test/datatypes/t2.bpl.expect | 5 |
7 files changed, 22 insertions, 4 deletions
diff --git a/Test/datatypes/Answer b/Test/datatypes/Answer index bac8f345..5624c30f 100644 --- a/Test/datatypes/Answer +++ b/Test/datatypes/Answer @@ -1,15 +1,15 @@ -------------------- t1.bpl --------------------
-t1.bpl(23,3): Error BP5001: This assertion might not hold.
+t1.bpl(25,3): Error BP5001: This assertion might not hold.
Execution trace:
- t1.bpl(16,3): anon0
+ t1.bpl(18,3): anon0
Boogie program verifier finished with 0 verified, 1 error
-------------------- t2.bpl --------------------
-t2.bpl(23,3): Error BP5001: This assertion might not hold.
+t2.bpl(25,3): Error BP5001: This assertion might not hold.
Execution trace:
- t2.bpl(16,3): anon0
+ t2.bpl(18,3): anon0
Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/datatypes/ex.bpl b/Test/datatypes/ex.bpl index 32b302f3..854119e0 100644 --- a/Test/datatypes/ex.bpl +++ b/Test/datatypes/ex.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -typeEncoding:m %s > %t
+// RUN: %diff %s.expect %t
type{:datatype} finite_map;
function{:constructor} finite_map(dom:[int]bool, map:[int]int):finite_map;
diff --git a/Test/datatypes/ex.bpl.expect b/Test/datatypes/ex.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/datatypes/ex.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/datatypes/t1.bpl b/Test/datatypes/t1.bpl index b56e26ae..77276bb8 100644 --- a/Test/datatypes/t1.bpl +++ b/Test/datatypes/t1.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -typeEncoding:m %s > %t
+// RUN: %diff %s.expect %t
type TT;
type {:datatype} Tree;
function {:constructor} leaf() : Tree;
diff --git a/Test/datatypes/t1.bpl.expect b/Test/datatypes/t1.bpl.expect new file mode 100644 index 00000000..22a24f0e --- /dev/null +++ b/Test/datatypes/t1.bpl.expect @@ -0,0 +1,5 @@ +t1.bpl(25,3): Error BP5001: This assertion might not hold. +Execution trace: + t1.bpl(18,3): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/datatypes/t2.bpl b/Test/datatypes/t2.bpl index d4d2bf3f..227ceb41 100644 --- a/Test/datatypes/t2.bpl +++ b/Test/datatypes/t2.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -typeEncoding:m %s > %t
+// RUN: %diff %s.expect %t
type TT;
type {:datatype} Tree;
function {:constructor} leaf`0() : Tree;
diff --git a/Test/datatypes/t2.bpl.expect b/Test/datatypes/t2.bpl.expect new file mode 100644 index 00000000..0d7a3cbb --- /dev/null +++ b/Test/datatypes/t2.bpl.expect @@ -0,0 +1,5 @@ +t2.bpl(25,3): Error BP5001: This assertion might not hold. +Execution trace: + t2.bpl(18,3): anon0 + +Boogie program verifier finished with 0 verified, 1 error |