diff options
| author |  schaef <unknown> | 2009-11-02 13:23:48 +0000 |
|---|---|---|
| committer | schaef <unknown> | 2009-11-02 13:23:48 +0000 |
| commit | 1787f47733a1f656b95e14ba881d7c3089b1b048 (patch) | |
| tree | 5a5708eb988a33269f18ed66bfdc23452785c254 /Test/doomed | |
| parent | eb1598e70398a9449613dbce7b3f4617b6558eb0 (diff) | |
vc:doomed does not use the console anymore to report results
added first test cases for doomed (including the ones from smoke)
minor bug fixes
minor speed-ups
Diffstat (limited to 'Test/doomed')
| -rw-r--r-- | Test/doomed/runtest.bat | 11 | ||||
| -rw-r--r-- | Test/doomed/smoke0.bpl | 79 |
2 files changed, 90 insertions, 0 deletions
diff --git a/Test/doomed/runtest.bat b/Test/doomed/runtest.bat new file mode 100644 index 00000000..215804cf --- /dev/null +++ b/Test/doomed/runtest.bat @@ -0,0 +1,11 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set BGEXE=%BOOGIEDIR%\Boogie.exe
+
+for %%f in (smoke0.bpl) do (
+ echo -------------------- %%f --------------------
+ %BGEXE% /vc:doomed %* %%f
+)
+
diff --git a/Test/doomed/smoke0.bpl b/Test/doomed/smoke0.bpl new file mode 100644 index 00000000..db01233f --- /dev/null +++ b/Test/doomed/smoke0.bpl @@ -0,0 +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;
+ }
+}
+
+
+
+
|