diff options
| author |  qadeer <qadeer@microsoft.com> | 2011-11-24 14:22:33 -0800 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2011-11-24 14:22:33 -0800 |
| commit | 132b03c3c6032dd2db21eac27616f7212dbcbb52 (patch) | |
| tree | 21c8197f2c15c92a1b9ab65d6b0b926221975dc2 /Test/houdini | |
| parent | df1cd695daffb01a590a7310dbee1b6594de2ecd (diff) | |
added some more statistics to houdini
added a coupe more regressions for houdini+inlineDepth
Diffstat (limited to 'Test/houdini')
| -rw-r--r-- | Test/houdini/Answer | 16 | ||||
| -rw-r--r-- | Test/houdini/runtest.bat | 2 | ||||
| -rw-r--r-- | Test/houdini/test1.bpl | 36 | ||||
| -rw-r--r-- | Test/houdini/test2.bpl | 38 |
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;
+
|