From ae44269a34b002797b2583b93a0041059b57cbda Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 27 Oct 2011 14:22:08 -0700 Subject: Boogie: Eliminated the /bv option. Only native bitvectors are supported now. The :forceBvZ3Native, :forceBvInt, and :bvint attributes were also eliminated. --- Test/stratifiedinline/Answer | 66 ++++++++++++++++++++++---------------------- 1 file changed, 33 insertions(+), 33 deletions(-) (limited to 'Test/stratifiedinline') diff --git a/Test/stratifiedinline/Answer b/Test/stratifiedinline/Answer index 290059d6..aee2722e 100644 --- a/Test/stratifiedinline/Answer +++ b/Test/stratifiedinline/Answer @@ -2,31 +2,31 @@ bar1.bpl(25,1): Error BP5003: A postcondition might not hold on this return path. 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 + 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 + bar2.bpl(19,3): anon0 + Inlined call to procedure foo begins + bar2.bpl(5,3): anon0 + bar2.bpl(9,7): anon3_Else + Inlined call to procedure foo ends + Inlined call to procedure foo begins + bar2.bpl(5,3): anon0 + bar2.bpl(6,7): anon3_Then + Inlined call to procedure foo ends Boogie program verifier finished with 0 verified, 1 error ----- @@ -34,23 +34,23 @@ Boogie program verifier finished with 0 verified, 1 error bar3.bpl(41,1): Error BP5003: A postcondition might not hold on this return path. 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 + 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(10,7): anon3_Else + 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 ----- -- cgit v1.2.3