replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

explanation that backjumps are counted when unwinding 

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3542 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
This commit is contained in:
kroening 2014-01-22 16:04:14 +00:00
parent 8a9ac1d283
commit ccdb07571b
1 changed files with 23 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

27
doc/html-manual/cbmc-loops.shtml
View File

@ -83,10 +83,10 @@ int main() {<br>
<hr>
<p class="justified">
One hundred iterations are obviously sufficient for the program above,
but note that the loop may abort prematurely depending on the value
that is returned by <code>f()</code>. CBMC is nevertheless able to automatically
unwind the loop to completion.</p>
The loop in the program above has an obvious upper bound on the number of
iterations, but note that the loop may abort prematurely depending on the
value that is returned by <code>f()</code>. CBMC is nevertheless able to
automatically unwind the loop to completion.</p>
<p class="justified">
This automatic detection of the unwinding
@ -98,6 +98,21 @@ CBMC offers the command-line option <code>--unwind B</code>, where
of loop unwindings CBMC performs on any loop.
</p>
This automatic detection of the unwinding
bound may fail if the number of loop iterations is highly data-dependent.
Furthermore, the number of iterations that are executed by any given
loop may be too large or may simply be unbounded. For this case,
CBMC offers the command-line option <code>--unwind B</code>, where
<code>B</code> denotes a number that corresponds to the maximal number
of loop unwindings CBMC performs on any loop.
</p>
<p class="justified">
Note that the number of unwindings is measured by counting the number of
<i>backjumps</i>. In the example above, note that the condition
<code>i<100</code> is in fact evaluated 101 times before the loop
terminates. Thus, the loop requires a limit of 101, and not 100.</p>
<h4>Setting Separate Unwinding Limits</h4>
<p class="justified">
@ -120,6 +135,10 @@ use
&nbsp;&nbsp;--unwindset L:B,L:B,...
</code>
<p>
where <code>L</code> denotes a loop ID and <code>B</code> denotes
the bound for that loop.</p>
<p class="justified">
As an example, consider a program with two loops in the function
main: