From 962f8d5252b3f5ec4d19e0cd2a430934bd55cc6d Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 28 Jun 2015 01:44:30 +0100 Subject: 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. --- Test/doomed/doomdebug.bpl | 88 +++++++++++------------ Test/doomed/doomed.bpl | 174 +++++++++++++++++++++++----------------------- Test/doomed/notdoomed.bpl | 116 +++++++++++++++---------------- Test/doomed/runtest.bat | 32 ++++----- Test/doomed/smoke0.bpl | 158 ++++++++++++++++++++--------------------- 5 files changed, 284 insertions(+), 284 deletions(-) (limited to 'Test/doomed') 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 j10) { - 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 j10) { + 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; + } +} + + + + -- cgit v1.2.3