From ce1c2de044c91624370411e23acab13b0381949b Mon Sep 17 00:00:00 2001
From: mikebarnett <unknown>
Date: Wed, 15 Jul 2009 21:03:41 +0000
Subject: Initial set of files.

---
 Test/smoke/Answer      | 25 ++++++++++++++++++++++++
 Test/smoke/Output      | 25 ++++++++++++++++++++++++
 Test/smoke/runtest.bat | 11 +++++++++++
 Test/smoke/smoke0.bpl  | 53 ++++++++++++++++++++++++++++++++++++++++++++++++++
 4 files changed, 114 insertions(+)
 create mode 100644 Test/smoke/Answer
 create mode 100644 Test/smoke/Output
 create mode 100644 Test/smoke/runtest.bat
 create mode 100644 Test/smoke/smoke0.bpl

(limited to 'Test/smoke')

diff --git a/Test/smoke/Answer b/Test/smoke/Answer
new file mode 100644
index 00000000..4141bdb0
--- /dev/null
+++ b/Test/smoke/Answer
@@ -0,0 +1,25 @@
+-------------------- smoke0.bpl --------------------
+found unreachable code:
+implementation b(x: int)
+{
+  var y: int;
+  var y@0: int;
+
+
+  anon0:
+    assume true;
+    assume true;
+    goto anon3_Then;
+
+  anon3_Then:
+    assume true;
+    assume x < 0;
+    y := 1;
+    assume 1 <= y && y <= 1;
+    assert false;
+    return;
+}
+
+
+
+Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/smoke/Output b/Test/smoke/Output
new file mode 100644
index 00000000..4141bdb0
--- /dev/null
+++ b/Test/smoke/Output
@@ -0,0 +1,25 @@
+-------------------- smoke0.bpl --------------------
+found unreachable code:
+implementation b(x: int)
+{
+  var y: int;
+  var y@0: int;
+
+
+  anon0:
+    assume true;
+    assume true;
+    goto anon3_Then;
+
+  anon3_Then:
+    assume true;
+    assume x < 0;
+    y := 1;
+    assume 1 <= y && y <= 1;
+    assert false;
+    return;
+}
+
+
+
+Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/smoke/runtest.bat b/Test/smoke/runtest.bat
new file mode 100644
index 00000000..7728d5ef
--- /dev/null
+++ b/Test/smoke/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% /smoke %* %%f
+)
+
diff --git a/Test/smoke/smoke0.bpl b/Test/smoke/smoke0.bpl
new file mode 100644
index 00000000..85deb324
--- /dev/null
+++ b/Test/smoke/smoke0.bpl
@@ -0,0 +1,53 @@
+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;
+  }
+}
+
+
-- 
cgit v1.2.3