summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar qadeer <qadeer@microsoft.com>2011-11-24 14:22:33 -0800
committerGravatar qadeer <qadeer@microsoft.com>2011-11-24 14:22:33 -0800
commit132b03c3c6032dd2db21eac27616f7212dbcbb52 (patch)
tree21c8197f2c15c92a1b9ab65d6b0b926221975dc2 /Test
parentdf1cd695daffb01a590a7310dbee1b6594de2ecd (diff)
added some more statistics to houdini
added a coupe more regressions for houdini+inlineDepth
Diffstat (limited to 'Test')
-rw-r--r--Test/houdini/Answer16
-rw-r--r--Test/houdini/runtest.bat2
-rw-r--r--Test/houdini/test1.bpl36
-rw-r--r--Test/houdini/test2.bpl38
4 files changed, 91 insertions, 1 deletions
diff --git a/Test/houdini/Answer b/Test/houdini/Answer
index 60ae7d80..474d1b09 100644
--- a/Test/houdini/Answer
+++ b/Test/houdini/Answer
@@ -100,6 +100,22 @@ b7 = False
Boogie program verifier finished with 1 verified, 0 errors
.
+-------------------- test1.bpl --------------------
+Assignment computed by Houdini:
+b0 = True
+b1 = False
+b2 = False
+
+Boogie program verifier finished with 4 verified, 0 errors
+.
+-------------------- test2.bpl --------------------
+Assignment computed by Houdini:
+b0 = True
+b1 = False
+b2 = False
+
+Boogie program verifier finished with 4 verified, 0 errors
+.
-------------------- test7.bpl --------------------
Assignment computed by Houdini:
diff --git a/Test/houdini/runtest.bat b/Test/houdini/runtest.bat
index 40f8cea0..aeffcd12 100644
--- a/Test/houdini/runtest.bat
+++ b/Test/houdini/runtest.bat
@@ -9,7 +9,7 @@ for %%f in (houd1.bpl houd2.bpl houd3.bpl houd4.bpl houd5.bpl houd6.bpl houd7.bp
%BGEXE% %* /nologo /noinfer /contractInfer %%f
)
-for %%f in (test7.bpl test8.bpl) do (
+for %%f in (test1.bpl test2.bpl test7.bpl test8.bpl) do (
echo .
echo -------------------- %%f --------------------
%BGEXE% %* /nologo /noinfer /contractInfer /inline:spec /inlineDepth:1 %%f
diff --git a/Test/houdini/test1.bpl b/Test/houdini/test1.bpl
new file mode 100644
index 00000000..e6ce06c9
--- /dev/null
+++ b/Test/houdini/test1.bpl
@@ -0,0 +1,36 @@
+var g: bool;
+
+procedure foo()
+modifies g;
+ensures b0 ==> (!old(g) ==> old(g) == g);
+{
+ call AcquireLock();
+ call ReleaseLock();
+}
+
+procedure AcquireLock()
+modifies g;
+ensures b1 ==> old(g) == g;
+{
+ g := true;
+}
+
+procedure ReleaseLock()
+modifies g;
+ensures b2 ==> old(g) == g;
+{
+ g := false;
+}
+
+procedure main()
+modifies g;
+{
+ g := false;
+ call foo();
+ assert !g;
+}
+
+const {:existential true} b0: bool;
+const {:existential true} b1: bool;
+const {:existential true } b2: bool;
+
diff --git a/Test/houdini/test2.bpl b/Test/houdini/test2.bpl
new file mode 100644
index 00000000..febb28e6
--- /dev/null
+++ b/Test/houdini/test2.bpl
@@ -0,0 +1,38 @@
+var g: int;
+var h: int;
+
+procedure foo()
+modifies g, h;
+ensures b0 ==> old(g) == g;
+{
+ call AcquireLock();
+ call ReleaseLock();
+}
+
+procedure AcquireLock()
+modifies g, h;
+ensures b1 ==> old(g) == g;
+{
+ h := g;
+ g := 1;
+}
+
+procedure ReleaseLock()
+modifies g, h;
+ensures b2 ==> old(g) == g;
+{
+ g := h;
+}
+
+procedure main()
+modifies g, h;
+{
+ g := 0;
+ call foo();
+ assert g == 0;
+}
+
+const {:existential true} b0: bool;
+const {:existential true} b1: bool;
+const {:existential true } b2: bool;
+