From 3ff2e42970584ad66f8b8e353ddce86dbea92baf Mon Sep 17 00:00:00 2001 From: qadeer Date: Wed, 4 Apr 2012 09:34:14 -0700 Subject: small fix added regressions --- Test/stratifiedinline/Answer | 422 ++++++++++++++++++++++++++++++++++++++ Test/stratifiedinline/bar10.bpl | 41 ++++ Test/stratifiedinline/bar7.bpl | 2 +- Test/stratifiedinline/bar8.bpl | 2 +- Test/stratifiedinline/bar9.bpl | 45 ++++ Test/stratifiedinline/runtest.bat | 12 ++ 6 files changed, 522 insertions(+), 2 deletions(-) create mode 100644 Test/stratifiedinline/bar10.bpl create mode 100644 Test/stratifiedinline/bar9.bpl (limited to 'Test/stratifiedinline') diff --git a/Test/stratifiedinline/Answer b/Test/stratifiedinline/Answer index aee2722e..6e23c098 100644 --- a/Test/stratifiedinline/Answer +++ b/Test/stratifiedinline/Answer @@ -62,3 +62,425 @@ Boogie program verifier finished with 1 verified, 0 errors Boogie program verifier finished with 1 verified, 0 errors ----- +----- Running regression test bar7.bpl +bar7.bpl(42,3): Error BP5001: This assertion might not hold. +Execution trace: + bar7.bpl(35,5): anon0 + bar7.bpl(37,5): anon4_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar7.bpl(7,3): anon0 + bar7.bpl(7,3): anon2_Else + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + bar7.bpl(42,3): anon3 + +Boogie program verifier finished with 0 verified, 1 error +----- +----- Running regression test bar8.bpl +bar8.bpl(41,3): Error BP5001: This assertion might not hold. +Execution trace: + bar8.bpl(34,5): anon0 + bar8.bpl(36,5): anon4_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar8.bpl(7,3): anon0 + bar8.bpl(7,3): anon2_Else + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + bar8.bpl(41,3): anon3 + +Boogie program verifier finished with 0 verified, 1 error +----- +----- Running regression test bar9.bpl +bar9.bpl(44,3): Error BP5001: This assertion might not hold. +Execution trace: + bar9.bpl(35,5): anon0 + bar9.bpl(41,5): anon4_Else + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(18,7): anon2_Then + Inlined call to procedure bar1 begins + bar9.bpl(16,3): anon0 + bar9.bpl(16,3): anon2_Else + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar1 ends + Inlined call to procedure bar2 begins + bar9.bpl(26,3): anon0 + bar9.bpl(27,7): anon2_Then + Inlined call to procedure bar2 begins + bar9.bpl(26,3): anon0 + bar9.bpl(27,7): anon2_Then + Inlined call to procedure bar2 begins + bar9.bpl(26,3): anon0 + bar9.bpl(27,7): anon2_Then + Inlined call to procedure bar2 begins + bar9.bpl(26,3): anon0 + bar9.bpl(27,7): anon2_Then + Inlined call to procedure bar2 begins + bar9.bpl(26,3): anon0 + bar9.bpl(27,7): anon2_Then + Inlined call to procedure bar2 begins + bar9.bpl(26,3): anon0 + bar9.bpl(27,7): anon2_Then + Inlined call to procedure bar2 begins + bar9.bpl(26,3): anon0 + bar9.bpl(27,7): anon2_Then + Inlined call to procedure bar2 begins + bar9.bpl(26,3): anon0 + bar9.bpl(27,7): anon2_Then + Inlined call to procedure bar2 begins + bar9.bpl(26,3): anon0 + bar9.bpl(27,7): anon2_Then + Inlined call to procedure bar2 begins + bar9.bpl(26,3): anon0 + bar9.bpl(27,7): anon2_Then + Inlined call to procedure bar2 begins + bar9.bpl(26,3): anon0 + bar9.bpl(26,3): anon2_Else + Inlined call to procedure bar2 ends + Inlined call to procedure bar2 ends + Inlined call to procedure bar2 ends + Inlined call to procedure bar2 ends + Inlined call to procedure bar2 ends + Inlined call to procedure bar2 ends + Inlined call to procedure bar2 ends + Inlined call to procedure bar2 ends + Inlined call to procedure bar2 ends + Inlined call to procedure bar2 ends + Inlined call to procedure bar2 ends + bar9.bpl(44,3): anon3 + +Boogie program verifier finished with 0 verified, 1 error +----- +----- Running regression test bar10.bpl +bar10.bpl(40,3): Error BP5001: This assertion might not hold. +Execution trace: + bar10.bpl(35,5): anon0 + Inlined call to procedure bar1 begins + bar10.bpl(16,3): anon0 + bar10.bpl(16,3): anon2_Else + Inlined call to procedure bar1 ends + Inlined call to procedure bar2 begins + bar10.bpl(26,3): anon0 + bar10.bpl(26,3): anon2_Else + Inlined call to procedure bar2 ends + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(8,9): anon2_Then + Inlined call to procedure foo begins + bar10.bpl(7,3): anon0 + bar10.bpl(7,3): anon2_Else + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + Inlined call to procedure foo ends + +Boogie program verifier finished with 0 verified, 1 error +----- diff --git a/Test/stratifiedinline/bar10.bpl b/Test/stratifiedinline/bar10.bpl new file mode 100644 index 00000000..8cfcfc13 --- /dev/null +++ b/Test/stratifiedinline/bar10.bpl @@ -0,0 +1,41 @@ +var i: int; +var m: int; + +procedure {:inline 1} foo() +modifies i; +{ + if (i < 20) { + i := i + 1; + call foo(); + } +} + +procedure {:inline 1} bar1(j: int) +modifies i; +{ + if (j < 2*m) + { + i := i + 1; + call bar1(j+1); + } +} + +procedure {:inline 1} bar2(j: int) +modifies i; +{ + if (j < m) { + i := i - 1; + call bar2(j+1); + } +} + +procedure main() +modifies i; +{ + i := 0; + call bar1(0); + call bar2(0); + i := 0; + call foo(); + assert i < 10; +} \ No newline at end of file diff --git a/Test/stratifiedinline/bar7.bpl b/Test/stratifiedinline/bar7.bpl index 747510de..b28777bd 100644 --- a/Test/stratifiedinline/bar7.bpl +++ b/Test/stratifiedinline/bar7.bpl @@ -4,7 +4,7 @@ var m: int; procedure {:inline 1} foo() modifies i; { - if (i < 80) { + if (i < 20) { i := i + 1; call foo(); } diff --git a/Test/stratifiedinline/bar8.bpl b/Test/stratifiedinline/bar8.bpl index d447e3a7..e96655f3 100644 --- a/Test/stratifiedinline/bar8.bpl +++ b/Test/stratifiedinline/bar8.bpl @@ -4,7 +4,7 @@ var m: int; procedure {:inline 1} foo() modifies i; { - if (i < 80) { + if (i < 20) { i := i + 1; call foo(); } diff --git a/Test/stratifiedinline/bar9.bpl b/Test/stratifiedinline/bar9.bpl new file mode 100644 index 00000000..12de78ad --- /dev/null +++ b/Test/stratifiedinline/bar9.bpl @@ -0,0 +1,45 @@ +var i: int; +var m: int; + +procedure {:inline 1} foo(x: int) +modifies i; +{ + if (i < x) { + i := i + 1; + call foo(x); + } +} + +procedure {:inline 1} bar1(j: int) +modifies i; +{ + if (j < 2*m) + { + i := i + 1; + call bar1(j+1); + } +} + +procedure {:inline 1} bar2(j: int) +modifies i; +{ + if (j < m) { + i := i - 1; + call bar2(j+1); + } +} + +procedure main() +modifies i; +{ + i := 0; + if (*) { + call foo(20); + i := 0; + call foo(4); + } else { + call bar1(0); + call bar2(0); + } + assert i < 10; +} \ No newline at end of file diff --git a/Test/stratifiedinline/runtest.bat b/Test/stratifiedinline/runtest.bat index 194570d0..d731d605 100644 --- a/Test/stratifiedinline/runtest.bat +++ b/Test/stratifiedinline/runtest.bat @@ -19,4 +19,16 @@ echo ----- echo ----- Running regression test bar6.bpl %BGEXE% %* /noinfer /stratifiedInline:1 bar6.bpl echo ----- +echo ----- Running regression test bar7.bpl +%BGEXE% %* /noinfer /stratifiedInline:1 /nonUniformUnfolding bar7.bpl +echo ----- +echo ----- Running regression test bar8.bpl +%BGEXE% %* /noinfer /stratifiedInline:1 /nonUniformUnfolding bar8.bpl +echo ----- +echo ----- Running regression test bar9.bpl +%BGEXE% %* /noinfer /stratifiedInline:1 /nonUniformUnfolding bar9.bpl +echo ----- +echo ----- Running regression test bar10.bpl +%BGEXE% %* /noinfer /stratifiedInline:1 /nonUniformUnfolding bar10.bpl +echo ----- -- cgit v1.2.3