From 1787f47733a1f656b95e14ba881d7c3089b1b048 Mon Sep 17 00:00:00 2001
From: schaef <unknown>
Date: Mon, 2 Nov 2009 13:23:48 +0000
Subject: 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

---
 Test/doomed/runtest.bat | 11 +++++++
 Test/doomed/smoke0.bpl  | 79 +++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 90 insertions(+)
 create mode 100644 Test/doomed/runtest.bat
 create mode 100644 Test/doomed/smoke0.bpl

(limited to 'Test/doomed')

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;    
+  }
+}
+
+
+
+
-- 
cgit v1.2.3