diff options
Diffstat (limited to 'Test/test15')
-rw-r--r-- | Test/test15/CaptureState.bpl | 58 | ||||
-rw-r--r-- | Test/test15/CaptureState.bpl.expect | 18 | ||||
-rw-r--r-- | Test/test15/IntInModel.bpl | 10 | ||||
-rw-r--r-- | Test/test15/InterpretedFunctionTests.bpl | 38 | ||||
-rw-r--r-- | Test/test15/ModelTest.bpl | 24 | ||||
-rw-r--r-- | Test/test15/NullInModel.bpl | 14 |
6 files changed, 81 insertions, 81 deletions
diff --git a/Test/test15/CaptureState.bpl b/Test/test15/CaptureState.bpl index 113e0b6a..ba3345f5 100644 --- a/Test/test15/CaptureState.bpl +++ b/Test/test15/CaptureState.bpl @@ -1,29 +1,29 @@ -// RUN: %boogie "%s" -mv:- > "%t"
-// RUN: %diff "%s.expect" "%t"
-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;
- m := 7;
- assume {:captureState "end"} true;
-}
+// RUN: %boogie "%s" -mv:- > "%t" +// RUN: %diff "%s.expect" "%t" +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; + m := 7; + assume {:captureState "end"} true; +} diff --git a/Test/test15/CaptureState.bpl.expect b/Test/test15/CaptureState.bpl.expect index 5d9d41c5..6939fee4 100644 --- a/Test/test15/CaptureState.bpl.expect +++ b/Test/test15/CaptureState.bpl.expect @@ -14,17 +14,17 @@ $mv_state_const -> 3 F -> T@FieldName!val!0 Heap -> |T@[Ref,FieldName]Int!val!0| m -> **m -m@0 -> (- 276) -m@1 -> (- 275) -m@3 -> (- 275) +m@0 -> (- 2) +m@1 -> (- 1) +m@3 -> (- 1) r -> **r -r@0 -> (- 550) +r@0 -> (- 2) this -> T@Ref!val!0 x -> 719 y -> **y Select_[Ref,FieldName]$int -> { - |T@[Ref,FieldName]Int!val!0| T@Ref!val!0 T@FieldName!val!0 -> (- 276) - else -> (- 276) + |T@[Ref,FieldName]Int!val!0| T@Ref!val!0 T@FieldName!val!0 -> (- 2) + else -> (- 2) } $mv_state -> { 3 0 -> true @@ -49,13 +49,13 @@ tickleBool -> { *** STATE top *** END_STATE *** STATE then - m -> (- 276) + m -> (- 2) *** END_STATE *** STATE postUpdate0 - m -> (- 275) + m -> (- 1) *** END_STATE *** STATE end - r -> (- 550) + r -> (- 2) m -> 7 *** END_STATE *** END_MODEL diff --git a/Test/test15/IntInModel.bpl b/Test/test15/IntInModel.bpl index 55bc14d9..8fa2e2bb 100644 --- a/Test/test15/IntInModel.bpl +++ b/Test/test15/IntInModel.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -printModel:2 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure M (i: int) {
- assert i != 0;
-}
+// RUN: %boogie -printModel:2 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure M (i: int) { + assert i != 0; +} diff --git a/Test/test15/InterpretedFunctionTests.bpl b/Test/test15/InterpretedFunctionTests.bpl index 33db52ef..5712595e 100644 --- a/Test/test15/InterpretedFunctionTests.bpl +++ b/Test/test15/InterpretedFunctionTests.bpl @@ -1,19 +1,19 @@ -// RUN: %boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure addition(x: int, y: int) {
- assume x == 1;
- assume y == 2;
- assert x + y == 4;
-}
-
-procedure subtraction(x: int, y: int) {
- assume x == 1;
- assume y == 2;
- assert x - y == 4; //only shows x-y == -1 when run with /method:subtraction, WHY???
-}
-
-procedure multiplication(x: int, y: int) {
- assume x == 1;
- assume y == 2;
- assert x * y == 4;
-}
+// RUN: %boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure addition(x: int, y: int) { + assume x == 1; + assume y == 2; + assert x + y == 4; +} + +procedure subtraction(x: int, y: int) { + assume x == 1; + assume y == 2; + assert x - y == 4; //only shows x-y == -1 when run with /method:subtraction, WHY??? +} + +procedure multiplication(x: int, y: int) { + assume x == 1; + assume y == 2; + assert x * y == 4; +} diff --git a/Test/test15/ModelTest.bpl b/Test/test15/ModelTest.bpl index 7764cb41..31e21de0 100644 --- a/Test/test15/ModelTest.bpl +++ b/Test/test15/ModelTest.bpl @@ -1,12 +1,12 @@ -// RUN: %boogie -printModel:2 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure M (s : ref, r : ref) {
- var i : int, j : int;
- i := 0 + 1;
- j := i + 1;
- j := j + 1;
- j := j + 1;
- assert i == j;
- assert s == r;
-}
-type ref;
+// RUN: %boogie -printModel:2 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure M (s : ref, r : ref) { + var i : int, j : int; + i := 0 + 1; + j := i + 1; + j := j + 1; + j := j + 1; + assert i == j; + assert s == r; +} +type ref; diff --git a/Test/test15/NullInModel.bpl b/Test/test15/NullInModel.bpl index aa68b763..560f2952 100644 --- a/Test/test15/NullInModel.bpl +++ b/Test/test15/NullInModel.bpl @@ -1,7 +1,7 @@ -// RUN: %boogie -printModel:2 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure M (s: ref) {
- assert s != null;
-}
-type ref;
-const null: ref;
+// RUN: %boogie -printModel:2 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure M (s: ref) { + assert s != null; +} +type ref; +const null: ref; |