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/test0/AttributeParsing.bpl | |
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/test0/AttributeParsing.bpl')
-rw-r--r-- | Test/test0/AttributeParsing.bpl | 80 |
1 files changed, 40 insertions, 40 deletions
diff --git a/Test/test0/AttributeParsing.bpl b/Test/test0/AttributeParsing.bpl index afc0a88d..7372fcc4 100644 --- a/Test/test0/AttributeParsing.bpl +++ b/Test/test0/AttributeParsing.bpl @@ -1,40 +1,40 @@ -// RUN: %boogie -noVerify -print:- -env:0 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-type {:sourcefile "test.ssc"} T;
-
-function {:source "test.scc"} f(int) returns (int);
-
-const {:description "The largest integer value"} unique MAXINT: int;
-
-axiom {:naming "MyFavoriteAxiom"} (forall i: int :: {f(i)} f(i) == i+1);
-
-var {:description "memory"} $Heap: [ref, name]any;
-
-var {:sort_of_like_a_trigger (forall i: int :: true)} Bla: [ref, name]any;
-
-procedure {:use_impl 1} foo(x : int) returns(n : int);
-
-implementation {:id 1} foo(x : int) returns(n : int)
-{
- block1: return;
-}
-
-implementation {:id 2} foo(x : int) returns(n : int)
-{
- block1: return;
-}
-
-type ref, any, name;
-
-
-// allow \" and other backslashes rather liberally:
-
-procedure
- {:myAttribute
- "h\n\"ello\"",
- "again",
- "and\\" a\"gain\"",
- again}
-P();
-
-const again: int;
+// RUN: %boogie -noVerify -print:- -env:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type {:sourcefile "test.ssc"} T; + +function {:source "test.scc"} f(int) returns (int); + +const {:description "The largest integer value"} unique MAXINT: int; + +axiom {:naming "MyFavoriteAxiom"} (forall i: int :: {f(i)} f(i) == i+1); + +var {:description "memory"} $Heap: [ref, name]any; + +var {:sort_of_like_a_trigger (forall i: int :: true)} Bla: [ref, name]any; + +procedure {:use_impl 1} foo(x : int) returns(n : int); + +implementation {:id 1} foo(x : int) returns(n : int) +{ + block1: return; +} + +implementation {:id 2} foo(x : int) returns(n : int) +{ + block1: return; +} + +type ref, any, name; + + +// allow \" and other backslashes rather liberally: + +procedure + {:myAttribute + "h\n\"ello\"", + "again", + "and\\" a\"gain\"", + again} +P(); + +const again: int; |