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.