2009-04-10: Updated Reference Manual
Version 6.3 of the
Bound-T Reference Manual (pdf) was
published today on the Bound-T website.
This is a normal evolution of the reference manual
to document new functions of Bound-T. It is not a major
change. New features introduced include:
- The ability to identify program parts by source-code
position. When you write an assertion for a loop
or a call, you can now identify the loop or call by its
place in the source code, either directly by using the
line number of a source-code line, or indirectly by using
the name of a mark embedded at this point in the source
code. The new command-line option -mark filename
specifies the names of mark definition files that Bound-T
should use.
- The ability to assert bounds on the number of starts
of a loop. This sets bounds on the number of times the
flow of execution reaches the loop at all. For example,
asserting that a loop starts zero times means that
the loop is never reached (is infeasible). The reference
manual now shows the new outputs for this ability.
- The ability to define additional symbolic identifiers
for subprograms and variables. This can compensate
for symbols missing from the debugging information in
the target program executable and avoid the direct use
of raw machine addresses. The new command-line
option -symbols filename specifies the names of
symbol files that Bound-T should use. Symbols defined in
this way can be used on the Bound-T command line to
identify root subprograms and in assertions to identify
subprograms and variables. Bound-T uses them in its
output, too, in place of the corresponding machine
addresses.
