diff options
Diffstat (limited to 'Test/extractloops/detLoopExtract1.bpl')
-rw-r--r-- | Test/extractloops/detLoopExtract1.bpl | 30 |
1 files changed, 30 insertions, 0 deletions
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; +} |