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/LineResolve.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/LineResolve.bpl')
-rw-r--r-- | Test/test0/LineResolve.bpl | 90 |
1 files changed, 45 insertions, 45 deletions
diff --git a/Test/test0/LineResolve.bpl b/Test/test0/LineResolve.bpl index 39bf9983..cca5c4a5 100644 --- a/Test/test0/LineResolve.bpl +++ b/Test/test0/LineResolve.bpl @@ -1,45 +1,45 @@ -// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure P() {
-var x: int;
-x :=
-
- a+ // error: LineResolve.bpl(5,1)
-
- b+ // error: LineResolve.bpl(7,2)
-#line 12
-c+ // error: LineResolve.bpl(12,0)
- d+ // error: LineResolve.bpl(13,10)
-#line 12
-e+ // error: LineResolve.bpl(12,0)
-#line 2
-f+ // error: LineResolve.bpl(2,0)
-#line 1000
-#line 900
-g+ // error: LineResolve.bpl(900,0)
-
-#line 10 Abc.txt
-
- h+ // error: Abc.txt(11,3)
-
-i+ // error: Abc.txt(13,0)
-#line 98
-
-j+ // error: Abc.txt(99,0)
-
-#line 103 c:\Users\leino\Documents\Programs\MyClass.ssc
-
-k+ // error: c:\Users\leino\Documents\Programs\MyClass.ssc(104,0)
-
-#line -58
-
-#line 12 A B C . txt
-l+ // error: A B C . txt(12,0)
-
-0;
-}
-
-#line 100 LineResolve.bpl
-procedure ResolutionTest() {
- x := 0; // error: undeclared identifier (once upon a time, this used to crash Boogie)
-}
+// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure P() { +var x: int; +x := + + a+ // error: LineResolve.bpl(5,1) + + b+ // error: LineResolve.bpl(7,2) +#line 12 +c+ // error: LineResolve.bpl(12,0) + d+ // error: LineResolve.bpl(13,10) +#line 12 +e+ // error: LineResolve.bpl(12,0) +#line 2 +f+ // error: LineResolve.bpl(2,0) +#line 1000 +#line 900 +g+ // error: LineResolve.bpl(900,0) + +#line 10 Abc.txt + + h+ // error: Abc.txt(11,3) + +i+ // error: Abc.txt(13,0) +#line 98 + +j+ // error: Abc.txt(99,0) + +#line 103 c:\Users\leino\Documents\Programs\MyClass.ssc + +k+ // error: c:\Users\leino\Documents\Programs\MyClass.ssc(104,0) + +#line -58 + +#line 12 A B C . txt +l+ // error: A B C . txt(12,0) + +0; +} + +#line 100 LineResolve.bpl +procedure ResolutionTest() { + x := 0; // error: undeclared identifier (once upon a time, this used to crash Boogie) +} |