From 7552293514e40a6dcd9749d3668519d7d32049d5 Mon Sep 17 00:00:00 2001 From: Unknown Date: Fri, 1 Jun 2012 01:36:11 -0700 Subject: 1. Fix for free ensures in inlined procedures. Becomes a skip instead of an assume. 2. Fix for deterministic loop extraction, and a new regression. 3. All regressions (including Dafny) except houdini pass, it is most likely related to the free ensures change. --- Test/extractloops/Answer | 5 +++++ Test/extractloops/detLoopExtract1.bpl | 30 ++++++++++++++++++++++++++++++ Test/extractloops/runtest.bat | 3 +++ 3 files changed, 38 insertions(+) create mode 100644 Test/extractloops/detLoopExtract1.bpl (limited to 'Test/extractloops') diff --git a/Test/extractloops/Answer b/Test/extractloops/Answer index b9083fae..48ca65e9 100644 --- a/Test/extractloops/Answer +++ b/Test/extractloops/Answer @@ -88,3 +88,8 @@ Stratified Inlining: Reached recursion bound of 4 Boogie program verifier finished with 1 verified, 0 errors ----- +----- Running regression test detLoopExtract1.bpl with deterministicExtractLoops +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 new file mode 100644 index 00000000..8388cd57 --- /dev/null +++ b/Test/extractloops/detLoopExtract1.bpl @@ -0,0 +1,30 @@ +var g:int; + +procedure {:entrypoint} Foo(a:int) +requires a >= 0; +modifies g; +{ + var b: int; + b := 0; + g := a; + +LH: + goto L_true, L_false; + +L_true: + assume (b < a); + goto L6; + +L6: + b := b + 1; + g := 5; + goto LH; + +L_false: + assume (b >= a); + goto L_end; + +L_end: + assume (b != a); //modeling assert for stratified inlining + return; +} diff --git a/Test/extractloops/runtest.bat b/Test/extractloops/runtest.bat index 05bfae55..6bd151cb 100644 --- a/Test/extractloops/runtest.bat +++ b/Test/extractloops/runtest.bat @@ -19,4 +19,7 @@ echo ----- echo ----- Running regression test detLoopExtract.bpl with deterministicExtractLoops %BGEXE% %* /stratifiedInline:1 /extractLoops /removeEmptyBlocks:0 /coalesceBlocks:0 /deterministicExtractLoops /recursionBound:4 detLoopExtract.bpl echo ----- +echo ----- Running regression test detLoopExtract1.bpl with deterministicExtractLoops +%BGEXE% %* /stratifiedInline:1 /extractLoops /removeEmptyBlocks:0 /coalesceBlocks:0 /deterministicExtractLoops /recursionBound:4 detLoopExtract1.bpl +echo ----- -- cgit v1.2.3