summaryrefslogtreecommitdiff
path: root/Test/doomed
diff options
context:
space:
mode:
Diffstat (limited to 'Test/doomed')
-rw-r--r--Test/doomed/doomdebug.bpl88
-rw-r--r--Test/doomed/doomed.bpl174
-rw-r--r--Test/doomed/notdoomed.bpl116
-rw-r--r--Test/doomed/runtest.bat32
-rw-r--r--Test/doomed/smoke0.bpl158
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;
+ }
+}
+
+
+
+