diff options
| author |  qadeer <unknown> | 2010-05-28 18:27:38 +0000 |
|---|---|---|
| committer | qadeer <unknown> | 2010-05-28 18:27:38 +0000 |
| commit | 4453e362a1ed8449f9031454467cd67da5674451 (patch) | |
| tree | 72de1eba9d1f9db64ef9a1f3a9392ab6c44b9dab /Test/lazyinline | |
| parent | 3b8dca0b54c45519be8f7e0c4c1ac92824690d28 (diff) | |
added lazyinline to the regressions
Diffstat (limited to 'Test/lazyinline')
| -rw-r--r-- | Test/lazyinline/Answer | 64 | ||||
| -rw-r--r-- | Test/lazyinline/runtest.bat | 22 |
2 files changed, 86 insertions, 0 deletions
diff --git a/Test/lazyinline/Answer b/Test/lazyinline/Answer new file mode 100644 index 00000000..aa83b37c --- /dev/null +++ b/Test/lazyinline/Answer @@ -0,0 +1,64 @@ +----- Running regression test bar1.bpl
+bar1.bpl(25,1): Error BP5003: A postcondition might not hold at this return statement.
+bar1.bpl(21,1): Related location: This is the postcondition that might not hold.
+Execution trace:
+ bar1.bpl(24,3): anon0
+ Inlined call to procedure foo begins
+ bar1.bpl(13,5): anon0
+ Inlined call to procedure bar begins
+ bar1.bpl(7,5): anon0
+ Inlined call to procedure bar ends
+ Inlined call to procedure bar begins
+ bar1.bpl(7,5): anon0
+ Inlined call to procedure bar ends
+ Inlined call to procedure foo ends
+
+Boogie program verifier finished with 0 verified, 1 error
+-----
+----- Running regression test bar2.bpl
+bar2.bpl(21,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ bar2.bpl(19,3): anon0
+ Inlined call to procedure foo begins
+ bar2.bpl(5,3): anon0
+ bar2.bpl(6,7): anon3_Then
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo begins
+ bar2.bpl(5,3): anon0
+ bar2.bpl(9,7): anon3_Else
+ Inlined call to procedure foo ends
+
+Boogie program verifier finished with 0 verified, 1 error
+-----
+----- Running regression test bar3.bpl
+bar3.bpl(41,1): Error BP5003: A postcondition might not hold at this return statement.
+bar3.bpl(34,1): Related location: This is the postcondition that might not hold.
+Execution trace:
+ bar3.bpl(38,3): anon0
+ Inlined call to procedure foo begins
+ bar3.bpl(18,3): anon0
+ bar3.bpl(19,7): anon3_Then
+ Inlined call to procedure bar begins
+ bar3.bpl(7,3): anon0
+ bar3.bpl(8,7): anon3_Then
+ Inlined call to procedure bar ends
+ Inlined call to procedure bar begins
+ bar3.bpl(7,3): anon0
+ bar3.bpl(8,7): anon3_Then
+ Inlined call to procedure bar ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure bar begins
+ bar3.bpl(7,3): anon0
+ bar3.bpl(10,7): anon3_Else
+ Inlined call to procedure bar ends
+
+Boogie program verifier finished with 0 verified, 1 error
+-----
+----- Running regression test bar4.bpl
+
+Boogie program verifier finished with 1 verified, 0 errors
+-----
+----- Running regression test bar6.bpl
+
+Boogie program verifier finished with 1 verified, 0 errors
+-----
diff --git a/Test/lazyinline/runtest.bat b/Test/lazyinline/runtest.bat new file mode 100644 index 00000000..cd141606 --- /dev/null +++ b/Test/lazyinline/runtest.bat @@ -0,0 +1,22 @@ +@echo off
+setlocal
+
+set BGEXE=..\..\Binaries\Boogie.exe
+rem set BGEXE=mono ..\..\Binaries\Boogie.exe
+
+echo ----- Running regression test bar1.bpl
+%BGEXE% %* /noinfer /lazyInline:1 bar1.bpl
+echo -----
+echo ----- Running regression test bar2.bpl
+%BGEXE% %* /noinfer /lazyInline:1 bar2.bpl
+echo -----
+echo ----- Running regression test bar3.bpl
+%BGEXE% %* /noinfer /lazyInline:1 bar3.bpl
+echo -----
+echo ----- Running regression test bar4.bpl
+%BGEXE% %* /noinfer /lazyInline:1 bar4.bpl
+echo -----
+echo ----- Running regression test bar6.bpl
+%BGEXE% %* /noinfer /lazyInline:1 bar6.bpl
+echo -----
+
|