diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-06-28 01:44:30 +0100 |
---|---|---|
committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-06-28 01:44:30 +0100 |
commit | 962f8d5252b3f5ec4d19e0cd2a430934bd55cc6d (patch) | |
tree | 27d5f9b0d130c6c1a6758bc0b7456b0aa51e34e0 /Test/test15 | |
parent | e11d65009d0b4ba1327f5f5dd6b26367330611f0 (diff) |
Normalise line endings using a .gitattributes file. Unfortunately
this required that this commit globally modify most files. If you
want to use git blame to see the real author of a line use the
``-w`` flag so that whitespace changes are ignored.
Diffstat (limited to 'Test/test15')
-rw-r--r-- | Test/test15/CaptureState.bpl | 58 | ||||
-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 |
5 files changed, 72 insertions, 72 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/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; |