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.

1 files changed, 87 insertions, 87 deletions

diff --git a/Test/doomed/doomed.bpl b/Test/doomed/doomed.bpl
index 9dea47b7..b211a481 100644
--- a/Test/doomed/doomed.bpl
+++ b/Test/doomed/doomed.bpl
@@ -1,87 +1,87 @@
-// RUN: %boogie -vc:doomed %s

-procedure evilrequires(x:int)

-  requires x>0;

-{

-  var y : int;

-

-  if(x<0) {

-    y := 1;

-  } else {

-    y := 2;

-  }

-}

-

-

-procedure evilbranch(x:int)

-{

-  var y : int;

-

-  if(x<0) {

-    y := 1;

-  } else {

-    y := 2;

-  }

-  assume y!=2;

-  

-  assert x<0; 

-}

-

-

-procedure evilloop(x:int)

-{

-  var y : int;

-  y:=x;

-  while (y<100) {

-     y := y -1;

-  }

-}

-

-procedure evilnested(x:int)

-{

-	 var i : int;

-	 var j : int;

-	 i:=x-1;

-	 j:=1;

-	 while (i>=0) {

-		while (j<=i) {

-			assert j<x;

-			j := j+1;

-		}

-		i := i - 1;

-	 }

-}

-

-

-procedure evilpath(x:int)

-{

-  var y : int;

-  y:=0;

-  if (x>10) {

-    y:=3;

-  } else {

-    assert y!=0;

-  }

-}

-

-procedure evilcondition(x:int)

-{

-  var y : int;

-  y:=0;

-  if (x!=0) {

-    y:=3;

-  } else {

-    assert x!=0;

-  }

-}

-

-procedure evilensures(x:int) returns  ($result: int)

-  ensures $result>0;

-{

-  var y : int;

-

-  if(x<0) {

-    y := 1;

-  } else {

-    $result:=-1;

-  }

-}

+// RUN: %boogie -vc:doomed %s
+procedure evilrequires(x:int)
+  requires x>0;
+{
+  var y : int;
+
+  if(x<0) {
+    y := 1;
+  } else {
+    y := 2;
+  }
+}
+
+
+procedure evilbranch(x:int)
+{
+  var y : int;
+
+  if(x<0) {
+    y := 1;
+  } else {
+    y := 2;
+  }
+  assume y!=2;
+  
+  assert x<0; 
+}
+
+
+procedure evilloop(x:int)
+{
+  var y : int;
+  y:=x;
+  while (y<100) {
+     y := y -1;
+  }
+}
+
+procedure evilnested(x:int)
+{
+	 var i : int;
+	 var j : int;
+	 i:=x-1;
+	 j:=1;
+	 while (i>=0) {
+		while (j<=i) {
+			assert j<x;
+			j := j+1;
+		}
+		i := i - 1;
+	 }
+}
+
+
+procedure evilpath(x:int)
+{
+  var y : int;
+  y:=0;
+  if (x>10) {
+    y:=3;
+  } else {
+    assert y!=0;
+  }
+}
+
+procedure evilcondition(x:int)
+{
+  var y : int;
+  y:=0;
+  if (x!=0) {
+    y:=3;
+  } else {
+    assert x!=0;
+  }
+}
+
+procedure evilensures(x:int) returns  ($result: int)
+  ensures $result>0;
+{
+  var y : int;
+
+  if(x<0) {
+    y := 1;
+  } else {
+    $result:=-1;
+  }
+}