diff options
| author |  Dan Liew <daniel.liew@imperial.ac.uk> | 2014-05-07 19:36:02 +0100 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-05-07 19:36:02 +0100 |
| commit | 8702d84fd360d9c2f11da295d616af4738bfd09a (patch) | |
| tree | b3900efaeec0ffc53ab1a8c4a7e826ec66bc086d /Test/inline/InliningAndLoops.bpl.expect | |
| parent | 9f555ab92f7cfe9edab8f12277b27cdee1849c32 (diff) | |
Enabled the inline lit tests. In order to support expansion2.bpl
we now require the OutputCheck tool. The lit.site.cfg file has
been taught to require that this tool is in the user's PATH
before testing starts.
Diffstat (limited to 'Test/inline/InliningAndLoops.bpl.expect')
| -rw-r--r-- | Test/inline/InliningAndLoops.bpl.expect | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/Test/inline/InliningAndLoops.bpl.expect b/Test/inline/InliningAndLoops.bpl.expect new file mode 100644 index 00000000..b5c38542 --- /dev/null +++ b/Test/inline/InliningAndLoops.bpl.expect @@ -0,0 +1,14 @@ +InliningAndLoops.bpl(14,5): Error BP5001: This assertion might not hold. +Execution trace: + InliningAndLoops.bpl(7,10): anon0#3 + InliningAndLoops.bpl(8,3): anon4_LoopHead#3 + InliningAndLoops.bpl(10,5): anon4_LoopBody#3 + InliningAndLoops.bpl(10,5): anon4_LoopBody$1#3 + InliningAndLoops.bpl(8,3): anon4_LoopHead#2 + InliningAndLoops.bpl(10,5): anon4_LoopBody#2 + InliningAndLoops.bpl(10,5): anon4_LoopBody$1#2 + InliningAndLoops.bpl(8,3): anon4_LoopHead#1 + InliningAndLoops.bpl(8,3): anon4_LoopDone#3 + InliningAndLoops.bpl(14,5): anon5_Then#3 + +Boogie program verifier finished with 0 verified, 1 error |