diff options
Diffstat (limited to 'Test/extractloops')
| -rw-r--r-- | Test/extractloops/Answer | 5 | ||||
| -rw-r--r-- | Test/extractloops/detLoopExtract1.bpl | 30 | ||||
| -rw-r--r-- | Test/extractloops/runtest.bat | 3 |
3 files changed, 38 insertions, 0 deletions
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 -----
|