diff options
| author |  mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
|---|---|---|
| committer | mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
| commit | ce1c2de044c91624370411e23acab13b0381949b (patch) | |
| tree | 592539996fe08050ead5ee210c973801611dde40 /Test/aitest0 | |
Initial set of files.
Diffstat (limited to 'Test/aitest0')
| -rw-r--r-- | Test/aitest0/Answer | 111 | ||||
| -rw-r--r-- | Test/aitest0/Output | 111 | ||||
| -rw-r--r-- | Test/aitest0/constants.bpl | 69 | ||||
| -rw-r--r-- | Test/aitest0/runtest.bat | 6 |
4 files changed, 297 insertions, 0 deletions
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
|