From 962f8d5252b3f5ec4d19e0cd2a430934bd55cc6d Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 28 Jun 2015 01:44:30 +0100 Subject: 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. --- Test/test15/CaptureState.bpl | 58 ++++++++++++++++++++++---------------------- 1 file changed, 29 insertions(+), 29 deletions(-) (limited to 'Test/test15/CaptureState.bpl') 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; +} -- cgit v1.2.3