Merging complete. Everything looks good *crosses fingers*

5 files changed, 284 insertions, 284 deletions

diff --git a/Test/doomed/doomdebug.bpl b/Test/doomed/doomdebug.bpl
index 0f45c13c..ef89e9dc 100644
--- a/Test/doomed/doomdebug.bpl
+++ b/Test/doomed/doomdebug.bpl
@@ -1,44 +1,44 @@
-procedure badtrace(x:int, y:int, z:int)

-{

-  var xin : int;

-  xin := x+z;

-

-  

-  if (y>5) {

-	xin:=5;

-  } else {

-	assert xin != x;

-  }

-}

-

-procedure baddiamond(x:int, y:int, z:int)

-{

-	var xin : int;

-	var yin : int;

-	var zin : int;

-	xin := x;

-	yin := y;

-	zin := z;

-	

-	if (y<5) {

-		xin := xin -3;		

-	} else {

-		zin := zin +10;

-		xin := 0;

-	}

-	

-	if (x<100) {

-		yin := 3;		

-	} else {

-		zin := 5;

-	}

-	

-	if (z>5) {

-		yin := yin - 2;

-		xin := xin + 3;

-	}

-

-	zin:=zin+yin;

-	

-	assert xin!=x;	

-}

+procedure badtrace(x:int, y:int, z:int)
+{
+  var xin : int;
+  xin := x+z;
+
+  
+  if (y>5) {
+	xin:=5;
+  } else {
+	assert xin != x;
+  }
+}
+
+procedure baddiamond(x:int, y:int, z:int)
+{
+	var xin : int;
+	var yin : int;
+	var zin : int;
+	xin := x;
+	yin := y;
+	zin := z;
+	
+	if (y<5) {
+		xin := xin -3;		
+	} else {
+		zin := zin +10;
+		xin := 0;
+	}
+	
+	if (x<100) {
+		yin := 3;		
+	} else {
+		zin := 5;
+	}
+	
+	if (z>5) {
+		yin := yin - 2;
+		xin := xin + 3;
+	}
+
+	zin:=zin+yin;
+	
+	assert xin!=x;	
+}
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;
+  }
+}
diff --git a/Test/doomed/notdoomed.bpl b/Test/doomed/notdoomed.bpl
index 8d57db71..321cf1eb 100644
--- a/Test/doomed/notdoomed.bpl
+++ b/Test/doomed/notdoomed.bpl
@@ -1,58 +1,58 @@
-// RUN: %boogie -vc:doomed %s

-procedure a(x:int)

-{

-  var y : int;

-

-  if(x<0) {

-    y := 1;

-  } else {

-    y := 2;

-  }

-}

-

-

-procedure b(x:int)

-{

-  var y : int;

-

-  if(x<0) {

-    y := 1;

-  } else {

-    y := 2;

-    assert false;

-  }

-}

-

-

-procedure c(x:int)

-{

-  var y : int;

-

-  if(x<0) {

-    y := 1;

-  } else {

-    y := 2;

-    assert {:PossiblyUnreachable} false;

-  }

-}

-

-procedure useCE(x:int)

-{

-  var y : int;

-

-  if(x<0) {

-    y := 1;

-  } else {

-    y := 2;

-  }

-  if(x<7) {    

-    y := 5;

-  } else {	

-    y := 6;

-  }

-

-}

-

-

-

-

+// RUN: %boogie -vc:doomed %s
+procedure a(x:int)
+{
+  var y : int;
+
+  if(x<0) {
+    y := 1;
+  } else {
+    y := 2;
+  }
+}
+
+
+procedure b(x:int)
+{
+  var y : int;
+
+  if(x<0) {
+    y := 1;
+  } else {
+    y := 2;
+    assert false;
+  }
+}
+
+
+procedure c(x:int)
+{
+  var y : int;
+
+  if(x<0) {
+    y := 1;
+  } else {
+    y := 2;
+    assert {:PossiblyUnreachable} false;
+  }
+}
+
+procedure useCE(x:int)
+{
+  var y : int;
+
+  if(x<0) {
+    y := 1;
+  } else {
+    y := 2;
+  }
+  if(x<7) {    
+    y := 5;
+  } else {	
+    y := 6;
+  }
+
+}
+
+
+
+
diff --git a/Test/doomed/runtest.bat b/Test/doomed/runtest.bat
index 9dda44cf..8c9364fb 100644
--- a/Test/doomed/runtest.bat
+++ b/Test/doomed/runtest.bat
@@ -1,16 +1,16 @@
-@echo off

-setlocal

-

-set BOOGIEDIR=..\..\Binaries

-set BGEXE=%BOOGIEDIR%\Boogie.exe

-

-for %%f in (doomed.bpl) do (

-  echo -------------------- %%f --------------------

-  %BGEXE% /vc:doomed %* %%f

-)

-

-for %%f in (notdoomed.bpl) do (

-  echo -------------------- %%f --------------------

-  %BGEXE% /vc:doomed %* %%f

-)

-

+@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set BGEXE=%BOOGIEDIR%\Boogie.exe
+
+for %%f in (doomed.bpl) do (
+  echo -------------------- %%f --------------------
+  %BGEXE% /vc:doomed %* %%f
+)
+
+for %%f in (notdoomed.bpl) do (
+  echo -------------------- %%f --------------------
+  %BGEXE% /vc:doomed %* %%f
+)
+
diff --git a/Test/doomed/smoke0.bpl b/Test/doomed/smoke0.bpl
index db01233f..159244ab 100644
--- a/Test/doomed/smoke0.bpl
+++ b/Test/doomed/smoke0.bpl
@@ -1,79 +1,79 @@
-procedure a(x:int)

-{

-  var y : int;

-

-  if(x<0) {

-    y := 1;

-  } else {

-    y := 2;

-  }

-}

-

-

-procedure b(x:int)

-  requires x>0;

-{

-  var y : int;

-

-  if(x<0) {

-    y := 1;

-  } else {

-    y := 2;

-  }

-}

-

-

-

-procedure c(x:int)

-  requires x>0;

-{

-  var y : int;

-

-  if(x<0) {

-    y := 1;

-    assert false;

-  } else {

-    y := 2;

-  }

-}

-

-procedure d(x:int)

-  requires x>0;

-{

-  var y : int;

-

-  if(x<0) {

-    assert false;

-    y := 1;

-  } else {

-    y := 2;

-  }

-}

-

-

-procedure doomed1(x:int)

-{

-  var y : int;

-  y := 0;

-  if(x<0) {

-    y := 1;

-  } else {

-    assert y!=0;

-  }

-}

-

-

-procedure doomed2(x:int)

-{

-  var y : int;

-  y := 0;

-  if(x!=0) {

-    y := 1;

-  } else {

-    assert x!=0;    

-  }

-}

-

-

-

-

+procedure a(x:int)
+{
+  var y : int;
+
+  if(x<0) {
+    y := 1;
+  } else {
+    y := 2;
+  }
+}
+
+
+procedure b(x:int)
+  requires x>0;
+{
+  var y : int;
+
+  if(x<0) {
+    y := 1;
+  } else {
+    y := 2;
+  }
+}
+
+
+
+procedure c(x:int)
+  requires x>0;
+{
+  var y : int;
+
+  if(x<0) {
+    y := 1;
+    assert false;
+  } else {
+    y := 2;
+  }
+}
+
+procedure d(x:int)
+  requires x>0;
+{
+  var y : int;
+
+  if(x<0) {
+    assert false;
+    y := 1;
+  } else {
+    y := 2;
+  }
+}
+
+
+procedure doomed1(x:int)
+{
+  var y : int;
+  y := 0;
+  if(x<0) {
+    y := 1;
+  } else {
+    assert y!=0;
+  }
+}
+
+
+procedure doomed2(x:int)
+{
+  var y : int;
+  y := 0;
+  if(x!=0) {
+    y := 1;
+  } else {
+    assert x!=0;    
+  }
+}
+
+
+
+