diff options
| author |  rustanleino <unknown> | 2010-08-10 02:16:29 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-08-10 02:16:29 +0000 |
| commit | 554fb3a6780c412b81dc935835c2760e4cbe0b4d (patch) | |
| tree | b50aa3dbbb369a52751bfcb9f142c9c928e591ae /Test/test15 | |
| parent | c2aa0b56fce36a101c3bef7ce901b8f26dcb5f08 (diff) | |
Boogie: Added boolean code expressions (sans well-formedness checks on the input).
Diffstat (limited to 'Test/test15')
| -rw-r--r-- | Test/test15/Answer | 27 |
1 files changed, 21 insertions, 6 deletions
diff --git a/Test/test15/Answer b/Test/test15/Answer index 2054998f..8452acb6 100644 --- a/Test/test15/Answer +++ b/Test/test15/Answer @@ -19,6 +19,11 @@ $pow2 -> { *8 -> *9
else -> #unspecified
}
+tickleBool -> {
+ *1 -> *0
+ *0 -> *0
+ else -> #unspecified
+}
Ctor -> {
*4 -> *8
*5 -> *9
@@ -50,7 +55,7 @@ False : *1 End of model.
NullInModel.bpl(2,3): Error BP5001: This assertion might not hold.
Execution trace:
- NullInModel.bpl(2,3): anon0
+ NullInModel.bpl(2,3): anon0
Boogie program verifier finished with 0 verified, 1 error
@@ -71,6 +76,11 @@ $pow2 -> { *6 -> *7
else -> #unspecified
}
+tickleBool -> {
+ *1 -> *0
+ *0 -> *0
+ else -> #unspecified
+}
Ctor -> {
*4 -> *6
*5 -> *7
@@ -94,7 +104,7 @@ False : *1 End of model.
IntInModel.bpl(2,3): Error BP5001: This assertion might not hold.
Execution trace:
- IntInModel.bpl(2,3): anon0
+ IntInModel.bpl(2,3): anon0
Boogie program verifier finished with 0 verified, 1 error
@@ -121,6 +131,11 @@ $pow2 -> { *13 -> *9
else -> #unspecified
}
+tickleBool -> {
+ *1 -> *0
+ *0 -> *0
+ else -> #unspecified
+}
Ctor -> {
*4 -> *13
*5 -> *9
@@ -159,19 +174,19 @@ False : *1 End of model.
ModelTest.bpl(7,3): Error BP5001: This assertion might not hold.
Execution trace:
- ModelTest.bpl(3,5): anon0
+ ModelTest.bpl(3,5): anon0
Boogie program verifier finished with 0 verified, 1 error
-------------------- InterpretedFunctionTests --------------------
InterpretedFunctionTests.bpl(4,3): Error BP5001: This assertion might not hold.
Execution trace:
- InterpretedFunctionTests.bpl(2,3): anon0
+ InterpretedFunctionTests.bpl(2,3): anon0
InterpretedFunctionTests.bpl(10,3): Error BP5001: This assertion might not hold.
Execution trace:
- InterpretedFunctionTests.bpl(8,3): anon0
+ InterpretedFunctionTests.bpl(8,3): anon0
InterpretedFunctionTests.bpl(16,3): Error BP5001: This assertion might not hold.
Execution trace:
- InterpretedFunctionTests.bpl(14,3): anon0
+ InterpretedFunctionTests.bpl(14,3): anon0
Boogie program verifier finished with 0 verified, 3 errors
|