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/aitest0/Answer        | 111 +++++++++++++++++++++++++++++++++++++++++++++
 Test/aitest0/Output        | 111 +++++++++++++++++++++++++++++++++++++++++++++
 Test/aitest0/constants.bpl |  69 ++++++++++++++++++++++++++++
 Test/aitest0/runtest.bat   |   6 +++
 4 files changed, 297 insertions(+)
 create mode 100644 Test/aitest0/Answer
 create mode 100644 Test/aitest0/Output
 create mode 100644 Test/aitest0/constants.bpl
 create mode 100644 Test/aitest0/runtest.bat

(limited to 'Test/aitest0')

diff --git a/Test/aitest0/Answer b/Test/aitest0/Answer
new file mode 100644
index 00000000..58750460
--- /dev/null
+++ b/Test/aitest0/Answer
@@ -0,0 +1,111 @@
+var GlobalFlag: bool;
+
+const A: int;
+
+const B: int;
+
+const C: int;
+
+procedure Join(b: bool);
+  modifies GlobalFlag;
+
+
+
+implementation Join(b: bool)
+{
+  var x: int;
+  var y: int;
+  var z: int;
+
+  start:
+    assume true;
+    GlobalFlag := true;
+    x := 3;
+    y := 4;
+    z := x + y;
+    assume x == 3 && y == 4 && z == 7;
+    goto Then, Else;
+
+  Then:
+    assume x == 3 && y == 4 && z == 7;
+    assume b <==> true;
+    x := x + 1;
+    assume x == 4 && y == 4 && z == 7;
+    goto join;
+
+  Else:
+    assume x == 3 && y == 4 && z == 7;
+    assume b <==> false;
+    y := 4;
+    assume x == 3 && y == 4 && z == 7;
+    goto join;
+
+  join:
+    assume y == 4 && z == 7;
+    assert y == 4;
+    assert z == 7;
+    assert GlobalFlag <==> true;
+    assume y == 4 && z == 7;
+    return;
+}
+
+
+
+procedure Loop();
+
+
+
+implementation Loop()
+{
+  var c: int;
+  var i: int;
+
+  start:
+    assume true;
+    c := 0;
+    i := 0;
+    assume c == 0 && i == 0;
+    goto test;
+
+  test:  // cut point
+    assume c == 0;
+    assume c == 0;
+    goto Then, Else;
+
+  Then:
+    assume c == 0;
+    assume i < 10;
+    i := i + 1;
+    assume c == 0;
+    goto test;
+
+  Else:
+    assume c == 0;
+    assume c == 0;
+    return;
+}
+
+
+
+procedure Evaluate();
+
+
+
+implementation Evaluate()
+{
+  var i: int;
+
+  start:
+    assume true;
+    i := 5;
+    i := 3 * i + 1;
+    i := 3 * (i + 1);
+    i := 1 + 3 * i;
+    i := (i + 1) * 3;
+    assume i == 465;
+    return;
+}
+
+
+
+Boogie program verifier finished with 0 verified, 0 errors
diff --git a/Test/aitest0/Output b/Test/aitest0/Output
new file mode 100644
index 00000000..58750460
--- /dev/null
+++ b/Test/aitest0/Output
@@ -0,0 +1,111 @@
+var GlobalFlag: bool;
+
+const A: int;
+
+const B: int;
+
+const C: int;
+
+procedure Join(b: bool);
+  modifies GlobalFlag;
+
+
+
+implementation Join(b: bool)
+{
+  var x: int;
+  var y: int;
+  var z: int;
+
+  start:
+    assume true;
+    GlobalFlag := true;
+    x := 3;
+    y := 4;
+    z := x + y;
+    assume x == 3 && y == 4 && z == 7;
+    goto Then, Else;
+
+  Then:
+    assume x == 3 && y == 4 && z == 7;
+    assume b <==> true;
+    x := x + 1;
+    assume x == 4 && y == 4 && z == 7;
+    goto join;
+
+  Else:
+    assume x == 3 && y == 4 && z == 7;
+    assume b <==> false;
+    y := 4;
+    assume x == 3 && y == 4 && z == 7;
+    goto join;
+
+  join:
+    assume y == 4 && z == 7;
+    assert y == 4;
+    assert z == 7;
+    assert GlobalFlag <==> true;
+    assume y == 4 && z == 7;
+    return;
+}
+
+
+
+procedure Loop();
+
+
+
+implementation Loop()
+{
+  var c: int;
+  var i: int;
+
+  start:
+    assume true;
+    c := 0;
+    i := 0;
+    assume c == 0 && i == 0;
+    goto test;
+
+  test:  // cut point
+    assume c == 0;
+    assume c == 0;
+    goto Then, Else;
+
+  Then:
+    assume c == 0;
+    assume i < 10;
+    i := i + 1;
+    assume c == 0;
+    goto test;
+
+  Else:
+    assume c == 0;
+    assume c == 0;
+    return;
+}
+
+
+
+procedure Evaluate();
+
+
+
+implementation Evaluate()
+{
+  var i: int;
+
+  start:
+    assume true;
+    i := 5;
+    i := 3 * i + 1;
+    i := 3 * (i + 1);
+    i := 1 + 3 * i;
+    i := (i + 1) * 3;
+    assume i == 465;
+    return;
+}
+
+
+
+Boogie program verifier finished with 0 verified, 0 errors
diff --git a/Test/aitest0/constants.bpl b/Test/aitest0/constants.bpl
new file mode 100644
index 00000000..3a47bfcd
--- /dev/null
+++ b/Test/aitest0/constants.bpl
@@ -0,0 +1,69 @@
+// Test the constant propagation AI
+
+var GlobalFlag : bool;
+
+const A, B, C:int;		// Consts
+
+procedure Join (b : bool)
+  modifies GlobalFlag;
+{  
+  var x, y, z:int;
+  
+  start:
+    GlobalFlag := true;
+    x := 3;
+    y := 4;
+    z := x + y;
+    goto Then, Else; // if (b)
+ 
+  Then:
+    assume b == true;
+    x := x + 1;
+    goto join;
+
+  Else:
+    assume b == false;
+    y := 4;
+    goto join;
+    
+  join:
+    assert y == 4;
+    assert z == 7;
+    assert GlobalFlag == true;
+    return;
+}    
+
+
+procedure Loop ()
+{
+  var c, i: int;
+
+  start:
+    c := 0; i := 0;
+    goto test;
+ 
+  test:
+    // if (i < 10);
+    goto Then, Else;
+
+  Then:
+    assume (i < 10);
+    i := i + 1;
+    goto test;
+
+  Else:
+    return;
+}
+
+procedure Evaluate () 
+{
+ var i : int;
+
+ start:
+ i := 5;
+ i := 3 * i + 1;
+ i := 3 * (i + 1);
+ i := 1 + 3 * i;
+ i := (i + 1) * 3;
+ return;
+}
diff --git a/Test/aitest0/runtest.bat b/Test/aitest0/runtest.bat
new file mode 100644
index 00000000..15f36ab0
--- /dev/null
+++ b/Test/aitest0/runtest.bat
@@ -0,0 +1,6 @@
+@echo off
+setlocal
+
+set BGEXE=..\..\Binaries\Boogie.exe
+
+%BGEXE% %* -infer:c -printInstrumented -noVerify constants.bpl
-- 
cgit v1.2.3