diff options
Diffstat (limited to 'Test/doomed')
| -rw-r--r-- | Test/doomed/doomdebug.bpl | 88 | ||||
| -rw-r--r-- | Test/doomed/doomed.bpl | 174 | ||||
| -rw-r--r-- | Test/doomed/notdoomed.bpl | 116 | ||||
| -rw-r--r-- | Test/doomed/runtest.bat | 32 | ||||
| -rw-r--r-- | Test/doomed/smoke0.bpl | 158 |
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; + } +} + + + + |