diff options
| author |  schaef <unknown> | 2009-11-18 15:23:19 +0000 |
|---|---|---|
| committer | schaef <unknown> | 2009-11-18 15:23:19 +0000 |
| commit | 62069bee7147d2f5ef620c0309ef1048ca95d0a7 (patch) | |
| tree | b0bff0f8f8e789d0f2b24588cf14255b0e46fe78 /Test | |
| parent | d64c97865ea76d67e0c9a0590a9a3b26bba10c9e (diff) | |
modified the doom checking. It is now able to report only the relevant statements and writes them the stdout. Line numbers are only displayed for bpl input.
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/doomed/doomed.bpl | 27 | ||||
| -rw-r--r-- | Test/doomed/notdoomed.bpl | 28 | ||||
| -rw-r--r-- | Test/doomed/runtest.bat | 7 |
3 files changed, 61 insertions, 1 deletions
diff --git a/Test/doomed/doomed.bpl b/Test/doomed/doomed.bpl new file mode 100644 index 00000000..a153e468 --- /dev/null +++ b/Test/doomed/doomed.bpl @@ -0,0 +1,27 @@ +
+procedure a(x:int)
+ requires x>0;
+{
+ 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 y!=2;
+}
+
+
diff --git a/Test/doomed/notdoomed.bpl b/Test/doomed/notdoomed.bpl new file mode 100644 index 00000000..86bf76d1 --- /dev/null +++ b/Test/doomed/notdoomed.bpl @@ -0,0 +1,28 @@ +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;
+ }
+}
+
+
+
+
+
diff --git a/Test/doomed/runtest.bat b/Test/doomed/runtest.bat index 215804cf..9dda44cf 100644 --- a/Test/doomed/runtest.bat +++ b/Test/doomed/runtest.bat @@ -4,7 +4,12 @@ setlocal set BOOGIEDIR=..\..\Binaries
set BGEXE=%BOOGIEDIR%\Boogie.exe
-for %%f in (smoke0.bpl) do (
+for %%f in (doomed.bpl) do (
+ echo -------------------- %%f --------------------
+ %BGEXE% /vc:doomed %* %%f
+)
+
+for %%f in (notdoomed.bpl) do (
echo -------------------- %%f --------------------
%BGEXE% /vc:doomed %* %%f
)
|