2010-02-07: Updated Assertion Language Manual
Version 6.4 of the
Bound-T Assertion Language Manual (pdf) was
published today on the Bound-T website.
This manual describes some small but important
updates of the assertion language.
New features introduced include:
- The ability to assert the "role" performed by
a specific instruction. For example, a return
instruction usually performs a return from the current
subprogram, but can also be used to perform a branch
or call to a dynamically computed address. Telling
Bound-T about such cases helps the analysis.
- The ability to identify subprograms by an address
offset from another subprogram. Some libraries
include local subprograms that have no public name that
could be used to identify assertions for that subprogram.
Such subprograms could be identified by their address, but
the address is different in different programs and also
changes from time to time in the same program, as the
program's memory map changes. The address offset
from a public library subprogram is a much more stable
means to identify such anonymous subprograms.
- The ability to assert that a subprogram returns to
an address that is offset by a constant amount from
the normal return point. Some compiler-specific
library subprograms have this departure from
the normal calling conventions, and are difficult to
analyse correctly without this new feature of the
assertion language.
For the convenience of users who are upgrading from the
earlier version (6.3) of the manual, a
manual with change bars is also available.