diff options
| author |  qadeer <qadeer@microsoft.com> | 2012-03-02 11:28:04 -0800 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2012-03-02 11:28:04 -0800 |
| commit | 7d1a42f0c26e2c7ba37a7de4b1ba3175777596c9 (patch) | |
| tree | 34a7e3cd5a47efb1657e83dc032b906b7f9be5b7 /Test | |
| parent | 9f31746b4fd5f491f56e04deb6addde5e600a659 (diff) | |
various refactorings related to houdini
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/houdini/Answer | 14 | ||||
| -rw-r--r-- | Test/houdini/runtest.bat | 4 |
2 files changed, 16 insertions, 2 deletions
diff --git a/Test/houdini/Answer b/Test/houdini/Answer index 6053b442..d7edbce6 100644 --- a/Test/houdini/Answer +++ b/Test/houdini/Answer @@ -9,6 +9,10 @@ Boogie program verifier finished with 1 verified, 0 errors Assignment computed by Houdini:
b1 = False
b2 = True
+houd2.bpl(12,1): Error BP5003: A postcondition might not hold on this return path.
+houd2.bpl(9,1): Related location: This is the postcondition that might not hold.
+Execution trace:
+ houd2.bpl(11,3): anon0
Boogie program verifier finished with 1 verified, 1 error
@@ -72,6 +76,9 @@ Assignment computed by Houdini: b1 = True
b2 = True
b3 = True
+houd9.bpl(19,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ houd9.bpl(18,9): anon0
Boogie program verifier finished with 0 verified, 1 error
@@ -80,11 +87,18 @@ Assignment computed by Houdini: b1 = True
b2 = True
b3 = True
+houd10.bpl(15,3): Error BP5002: A precondition for this call might not hold.
+houd10.bpl(20,1): Related location: This is the precondition that might not hold.
+Execution trace:
+ houd10.bpl(14,9): anon0
Boogie program verifier finished with 0 verified, 1 error
-------------------- houd11.bpl --------------------
Assignment computed by Houdini:
+houd11.bpl(8,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ houd11.bpl(7,9): anon0
Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/houdini/runtest.bat b/Test/houdini/runtest.bat index f0065b0d..b9816bb9 100644 --- a/Test/houdini/runtest.bat +++ b/Test/houdini/runtest.bat @@ -6,11 +6,11 @@ set BGEXE=..\..\Binaries\Boogie.exe for %%f in (houd1.bpl houd2.bpl houd3.bpl houd4.bpl houd5.bpl houd6.bpl houd7.bpl houd8.bpl houd9.bpl houd10.bpl houd11.bpl houd12.bpl) do (
echo.
echo -------------------- %%f --------------------
- %BGEXE% %* /nologo /noinfer /contractInfer %%f
+ %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment %%f
)
for %%f in (test1.bpl test2.bpl test7.bpl test8.bpl test9.bpl test10.bpl) do (
echo .
echo -------------------- %%f --------------------
- %BGEXE% %* /nologo /noinfer /contractInfer /inlineDepth:1 %%f
+ %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /inlineDepth:1 %%f
)
|