From 868c3ef5b53f0a07a4bd0f45b47269800564e251 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 7 May 2014 20:52:44 +0100 Subject: Enabled "Extract loops benchmarks" lit tests. --- Test/extractloops/Answer | 90 ++++++++++++++-------------- Test/extractloops/detLoopExtract.bpl | 4 +- Test/extractloops/detLoopExtract.bpl.expect | 3 + Test/extractloops/detLoopExtract1.bpl | 2 + Test/extractloops/detLoopExtract1.bpl.expect | 3 + Test/extractloops/t1.bpl | 2 + Test/extractloops/t1.bpl.expect | 21 +++++++ Test/extractloops/t2.bpl | 2 + Test/extractloops/t2.bpl.expect | 33 ++++++++++ Test/extractloops/t3.bpl | 4 ++ Test/extractloops/t3.bpl.rb2.expect | 2 + Test/extractloops/t3.bpl.rb4.expect | 21 +++++++ 12 files changed, 141 insertions(+), 46 deletions(-) create mode 100644 Test/extractloops/detLoopExtract.bpl.expect create mode 100644 Test/extractloops/detLoopExtract1.bpl.expect create mode 100644 Test/extractloops/t1.bpl.expect create mode 100644 Test/extractloops/t2.bpl.expect create mode 100644 Test/extractloops/t3.bpl.rb2.expect create mode 100644 Test/extractloops/t3.bpl.rb4.expect (limited to 'Test/extractloops') diff --git a/Test/extractloops/Answer b/Test/extractloops/Answer index 48ca65e9..88bd8c99 100644 --- a/Test/extractloops/Answer +++ b/Test/extractloops/Answer @@ -1,58 +1,58 @@ ----- Running regression test t1.bpl (0,0): Error BP5001: This assertion might not hold. Execution trace: - t1.bpl(17,3): anon0 - t1.bpl(22,3): anon3_LoopHead + t1.bpl(19,3): anon0 + t1.bpl(24,3): anon3_LoopHead Inlined call to procedure foo begins - t1.bpl(8,5): anon0 + t1.bpl(10,5): anon0 Inlined call to procedure foo ends - t1.bpl(26,3): anon3_LoopBody - t1.bpl(22,3): anon3_LoopHead + t1.bpl(28,3): anon3_LoopBody + t1.bpl(24,3): anon3_LoopHead Inlined call to procedure foo begins - t1.bpl(8,5): anon0 + t1.bpl(10,5): anon0 Inlined call to procedure foo ends - t1.bpl(26,3): anon3_LoopBody - t1.bpl(22,3): anon3_LoopHead + t1.bpl(28,3): anon3_LoopBody + t1.bpl(24,3): anon3_LoopHead Inlined call to procedure foo begins - t1.bpl(8,5): anon0 + t1.bpl(10,5): anon0 Inlined call to procedure foo ends - t1.bpl(32,3): anon3_LoopDone - t1.bpl(36,3): anon2 + t1.bpl(34,3): anon3_LoopDone + t1.bpl(38,3): anon2 Boogie program verifier finished with 0 verified, 1 error ----- ----- Running regression test t2.bpl (0,0): Error BP5001: This assertion might not hold. Execution trace: - t2.bpl(16,3): anon0 - t2.bpl(21,3): anon3_LoopHead + t2.bpl(18,3): anon0 + t2.bpl(23,3): anon3_LoopHead Inlined call to procedure foo begins - t2.bpl(7,5): anon0 + t2.bpl(9,5): anon0 Inlined call to procedure foo ends - t2.bpl(25,3): anon3_LoopBody - t2.bpl(32,3): lab1_LoopHead - t2.bpl(35,3): lab1_LoopBody - t2.bpl(32,3): lab1_LoopHead - t2.bpl(35,3): lab1_LoopBody - t2.bpl(32,3): lab1_LoopHead - t2.bpl(40,3): lab1_LoopDone - t2.bpl(21,3): anon3_LoopHead + t2.bpl(27,3): anon3_LoopBody + t2.bpl(34,3): lab1_LoopHead + t2.bpl(37,3): lab1_LoopBody + t2.bpl(34,3): lab1_LoopHead + t2.bpl(37,3): lab1_LoopBody + t2.bpl(34,3): lab1_LoopHead + t2.bpl(42,3): lab1_LoopDone + t2.bpl(23,3): anon3_LoopHead Inlined call to procedure foo begins - t2.bpl(7,5): anon0 + t2.bpl(9,5): anon0 Inlined call to procedure foo ends - t2.bpl(25,3): anon3_LoopBody - t2.bpl(32,3): lab1_LoopHead - t2.bpl(35,3): lab1_LoopBody - t2.bpl(32,3): lab1_LoopHead - t2.bpl(35,3): lab1_LoopBody - t2.bpl(32,3): lab1_LoopHead - t2.bpl(40,3): lab1_LoopDone - t2.bpl(21,3): anon3_LoopHead + t2.bpl(27,3): anon3_LoopBody + t2.bpl(34,3): lab1_LoopHead + t2.bpl(37,3): lab1_LoopBody + t2.bpl(34,3): lab1_LoopHead + t2.bpl(37,3): lab1_LoopBody + t2.bpl(34,3): lab1_LoopHead + t2.bpl(42,3): lab1_LoopDone + t2.bpl(23,3): anon3_LoopHead Inlined call to procedure foo begins - t2.bpl(7,5): anon0 + t2.bpl(9,5): anon0 Inlined call to procedure foo ends - t2.bpl(44,3): anon3_LoopDone - t2.bpl(48,3): anon2 + t2.bpl(46,3): anon3_LoopDone + t2.bpl(50,3): anon2 Boogie program verifier finished with 0 verified, 1 error ----- @@ -63,23 +63,23 @@ Boogie program verifier finished with 1 verified, 0 errors ----- Running regression test t3.bpl with recursion bound 4 (0,0): Error BP5001: This assertion might not hold. Execution trace: - t3.bpl(15,3): anon0 - t3.bpl(20,3): anon3_LoopHead + t3.bpl(19,3): anon0 + t3.bpl(24,3): anon3_LoopHead Inlined call to procedure foo begins - t3.bpl(6,5): anon0 + t3.bpl(10,5): anon0 Inlined call to procedure foo ends - t3.bpl(24,3): anon3_LoopBody - t3.bpl(20,3): anon3_LoopHead + t3.bpl(28,3): anon3_LoopBody + t3.bpl(24,3): anon3_LoopHead Inlined call to procedure foo begins - t3.bpl(6,5): anon0 + t3.bpl(10,5): anon0 Inlined call to procedure foo ends - t3.bpl(24,3): anon3_LoopBody - t3.bpl(20,3): anon3_LoopHead + t3.bpl(28,3): anon3_LoopBody + t3.bpl(24,3): anon3_LoopHead Inlined call to procedure foo begins - t3.bpl(6,5): anon0 + t3.bpl(10,5): anon0 Inlined call to procedure foo ends - t3.bpl(30,3): anon3_LoopDone - t3.bpl(34,3): anon2 + t3.bpl(34,3): anon3_LoopDone + t3.bpl(38,3): anon2 Boogie program verifier finished with 0 verified, 1 error ----- diff --git a/Test/extractloops/detLoopExtract.bpl b/Test/extractloops/detLoopExtract.bpl index 976d58d6..b224aece 100644 --- a/Test/extractloops/detLoopExtract.bpl +++ b/Test/extractloops/detLoopExtract.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -stratifiedInline:1 -extractLoops -removeEmptyBlocks:0 -coalesceBlocks:0 -deterministicExtractLoops -recursionBound:4 %s > %t +// RUN: %diff %s.expect %t var g:int; var h:int; //not modified var k:int; //modified in a procedure call @@ -41,4 +43,4 @@ modifies k; { k := 0; return; -} \ No newline at end of file +} diff --git a/Test/extractloops/detLoopExtract.bpl.expect b/Test/extractloops/detLoopExtract.bpl.expect new file mode 100644 index 00000000..0840bd8a --- /dev/null +++ b/Test/extractloops/detLoopExtract.bpl.expect @@ -0,0 +1,3 @@ +Stratified Inlining: Reached recursion bound of 4 + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/extractloops/detLoopExtract1.bpl b/Test/extractloops/detLoopExtract1.bpl index 8388cd57..80646ef2 100644 --- a/Test/extractloops/detLoopExtract1.bpl +++ b/Test/extractloops/detLoopExtract1.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -stratifiedInline:1 -extractLoops -removeEmptyBlocks:0 -coalesceBlocks:0 -deterministicExtractLoops -recursionBound:4 %s > %t +// RUN: %diff %s.expect %t var g:int; procedure {:entrypoint} Foo(a:int) diff --git a/Test/extractloops/detLoopExtract1.bpl.expect b/Test/extractloops/detLoopExtract1.bpl.expect new file mode 100644 index 00000000..0840bd8a --- /dev/null +++ b/Test/extractloops/detLoopExtract1.bpl.expect @@ -0,0 +1,3 @@ +Stratified Inlining: Reached recursion bound of 4 + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/extractloops/t1.bpl b/Test/extractloops/t1.bpl index 00df45e9..2f566a4c 100644 --- a/Test/extractloops/t1.bpl +++ b/Test/extractloops/t1.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -stratifiedInline:1 -extractLoops -removeEmptyBlocks:0 -coalesceBlocks:0 %s > %t +// RUN: %diff %s.expect %t var g: int; diff --git a/Test/extractloops/t1.bpl.expect b/Test/extractloops/t1.bpl.expect new file mode 100644 index 00000000..9780a21f --- /dev/null +++ b/Test/extractloops/t1.bpl.expect @@ -0,0 +1,21 @@ +(0,0): Error BP5001: This assertion might not hold. +Execution trace: + t1.bpl(19,3): anon0 + t1.bpl(24,3): anon3_LoopHead + Inlined call to procedure foo begins + t1.bpl(10,5): anon0 + Inlined call to procedure foo ends + t1.bpl(28,3): anon3_LoopBody + t1.bpl(24,3): anon3_LoopHead + Inlined call to procedure foo begins + t1.bpl(10,5): anon0 + Inlined call to procedure foo ends + t1.bpl(28,3): anon3_LoopBody + t1.bpl(24,3): anon3_LoopHead + Inlined call to procedure foo begins + t1.bpl(10,5): anon0 + Inlined call to procedure foo ends + t1.bpl(34,3): anon3_LoopDone + t1.bpl(38,3): anon2 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/extractloops/t2.bpl b/Test/extractloops/t2.bpl index 93f80f20..5546eb86 100644 --- a/Test/extractloops/t2.bpl +++ b/Test/extractloops/t2.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -stratifiedInline:1 -extractLoops -removeEmptyBlocks:0 -coalesceBlocks:0 %s > %t +// RUN: %diff %s.expect %t var g: int; diff --git a/Test/extractloops/t2.bpl.expect b/Test/extractloops/t2.bpl.expect new file mode 100644 index 00000000..27f59372 --- /dev/null +++ b/Test/extractloops/t2.bpl.expect @@ -0,0 +1,33 @@ +(0,0): Error BP5001: This assertion might not hold. +Execution trace: + t2.bpl(18,3): anon0 + t2.bpl(23,3): anon3_LoopHead + Inlined call to procedure foo begins + t2.bpl(9,5): anon0 + Inlined call to procedure foo ends + t2.bpl(27,3): anon3_LoopBody + t2.bpl(34,3): lab1_LoopHead + t2.bpl(37,3): lab1_LoopBody + t2.bpl(34,3): lab1_LoopHead + t2.bpl(37,3): lab1_LoopBody + t2.bpl(34,3): lab1_LoopHead + t2.bpl(42,3): lab1_LoopDone + t2.bpl(23,3): anon3_LoopHead + Inlined call to procedure foo begins + t2.bpl(9,5): anon0 + Inlined call to procedure foo ends + t2.bpl(27,3): anon3_LoopBody + t2.bpl(34,3): lab1_LoopHead + t2.bpl(37,3): lab1_LoopBody + t2.bpl(34,3): lab1_LoopHead + t2.bpl(37,3): lab1_LoopBody + t2.bpl(34,3): lab1_LoopHead + t2.bpl(42,3): lab1_LoopDone + t2.bpl(23,3): anon3_LoopHead + Inlined call to procedure foo begins + t2.bpl(9,5): anon0 + Inlined call to procedure foo ends + t2.bpl(46,3): anon3_LoopDone + t2.bpl(50,3): anon2 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/extractloops/t3.bpl b/Test/extractloops/t3.bpl index d14767ab..d3afa8d5 100644 --- a/Test/extractloops/t3.bpl +++ b/Test/extractloops/t3.bpl @@ -1,3 +1,7 @@ +// RUN: %boogie -stratifiedInline:1 -extractLoops -removeEmptyBlocks:0 -coalesceBlocks:0 -recursionBound:2 %s > %t +// RUN: %diff %s.rb2.expect %t +// RUN: %boogie -stratifiedInline:1 -extractLoops -removeEmptyBlocks:0 -coalesceBlocks:0 -recursionBound:4 %s > %t +// RUN: %diff %s.rb4.expect %t var g: int; procedure foo() diff --git a/Test/extractloops/t3.bpl.rb2.expect b/Test/extractloops/t3.bpl.rb2.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/extractloops/t3.bpl.rb2.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/extractloops/t3.bpl.rb4.expect b/Test/extractloops/t3.bpl.rb4.expect new file mode 100644 index 00000000..cdcdd0f2 --- /dev/null +++ b/Test/extractloops/t3.bpl.rb4.expect @@ -0,0 +1,21 @@ +(0,0): Error BP5001: This assertion might not hold. +Execution trace: + t3.bpl(19,3): anon0 + t3.bpl(24,3): anon3_LoopHead + Inlined call to procedure foo begins + t3.bpl(10,5): anon0 + Inlined call to procedure foo ends + t3.bpl(28,3): anon3_LoopBody + t3.bpl(24,3): anon3_LoopHead + Inlined call to procedure foo begins + t3.bpl(10,5): anon0 + Inlined call to procedure foo ends + t3.bpl(28,3): anon3_LoopBody + t3.bpl(24,3): anon3_LoopHead + Inlined call to procedure foo begins + t3.bpl(10,5): anon0 + Inlined call to procedure foo ends + t3.bpl(34,3): anon3_LoopDone + t3.bpl(38,3): anon2 + +Boogie program verifier finished with 0 verified, 1 error -- cgit v1.2.3