diff options
| author |  rustanleino <unknown> | 2010-09-23 02:03:11 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-09-23 02:03:11 +0000 |
| commit | a3d28fd0c7d454667b6bea71a34b89e47b66d611 (patch) | |
| tree | c8ab912181bd5b57ae8675744687a1feb1020273 /Test/test15 | |
| parent | 40021fe7042eb08ed5b4d16034e23c9ed022c4aa (diff) | |
Boogie:
* Added /mv flag as the start of a Boogie replacement for /cev
* Allow attributes on assume statements
* /mv looks for the assume-statement attribute :captureState with a string-literal argument
Diffstat (limited to 'Test/test15')
| -rw-r--r-- | Test/test15/Answer | 27 | ||||
| -rw-r--r-- | Test/test15/CaptureState.bpl | 26 | ||||
| -rw-r--r-- | Test/test15/runtest.bat | 4 |
3 files changed, 49 insertions, 8 deletions
diff --git a/Test/test15/Answer b/Test/test15/Answer index 8452acb6..969bbe41 100644 --- a/Test/test15/Answer +++ b/Test/test15/Answer @@ -55,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
@@ -104,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
@@ -174,19 +174,34 @@ 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
+
+-------------------- CaptureState --------------------
+CaptureState.bpl(26,1): Error BP5003: A postcondition might not hold on this return path.
+CaptureState.bpl(8,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ CaptureState.bpl(12,3): anon0
+ CaptureState.bpl(16,5): anon4_Then
+ CaptureState.bpl(24,5): anon3
+Captured states:
+ top
+ then
+ postUpdate0
+ end
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/test15/CaptureState.bpl b/Test/test15/CaptureState.bpl new file mode 100644 index 00000000..7c73c411 --- /dev/null +++ b/Test/test15/CaptureState.bpl @@ -0,0 +1,26 @@ +type Ref;
+type FieldName;
+var Heap: [Ref,FieldName]int;
+
+const unique F: FieldName;
+
+procedure P(this: Ref, x: int, y: int) returns (r: int)
+ ensures 0 <= r;
+{
+ var m: int;
+
+ assume {:captureState "top"} true;
+
+ m := Heap[this, F];
+ if (0 <= x) {
+ assume {:captureState "then"} true;
+ m := m + 1;
+ assume {:captureState "postUpdate0"} true;
+ } else {
+ assume {:captureState "else"} true;
+ m := (m + y) * (m + y);
+ assume {:captureState "postUpdate1"} true;
+ }
+ r := m + m;
+ assume {:captureState "end"} true;
+}
diff --git a/Test/test15/runtest.bat b/Test/test15/runtest.bat index 90771065..fc25c876 100644 --- a/Test/test15/runtest.bat +++ b/Test/test15/runtest.bat @@ -9,8 +9,8 @@ for %%f in (NullInModel IntInModel ModelTest) do ( echo -------------------- %%f --------------------
"%BGEXE%" %* %%f.bpl /printModel:2
)
-for %%f in (InterpretedFunctionTests) do (
+for %%f in (InterpretedFunctionTests CaptureState) do (
echo.
echo -------------------- %%f --------------------
- "%BGEXE%" %* %%f.bpl
+ "%BGEXE%" %* %%f.bpl
)
|