Specifications

3 WRITING ASSERTIONS
3.1 Overview
If you use Bound-T to analyse non-trivial programs you nearly always have to write assertions
to control and guide the analysis. The most common role of assertions is to set bounds on some
aspects of the behaviour of the target program, for example bounds on loop iterations, that
Bound-T cannot deduce automatically. Assertions must identify the relevant parts of the target
program, for example subprograms and variables. The Bound-T assertion language has a
generic high-level syntax [3] in which some elements with target-specific syntax appear as the
contents of quoted strings:
• subprogram names,
• code addresses and address offsets,
• variable names,
• data addresses and register names,
• stack names,
• instruction roles, and
• names of target-specific properties of program parts.
In practice the names (identifiers) of subprograms and variables are either identical to the
names used in the source code, or some “mangled” form of the source-code identifiers where
the mangling depends on the cross-compiler and not on Bound-T. However, Bound-T defines a
target-specific way to write the addresses of code and data in assertions. Register names are
considered a kind of “data address” and are target-specific.
This chapter continues the user-guide part of this Application Note by defining the H8/300-
specific aspects of the assertion language. This chapter explains any specific limitations and
possibilities for user-specified assertions when Bound-T is used with H8/300 programs.
3.2 Symbolic names
Linkage symbols
When the target program is compiled with debugging, the executable file usually contains a
symbol-table that Bound-T can use to connect the symbolic names of subprograms and
variables to their machine-level addresses for the analysis. You can then write assertions using
the symbolic names. (Executable files in S-record form are an exception and do not contain
any debugging information. The options -symbols or -sym can be used to define symbolic
names even for S-record files.)
As in most versions of Bound-T, you must use the linkage symbols, not the source-code
identifiers, to name subprograms and variables. Depending on the compiler and linker, the
linkage symbols may be the same as the source-code identifiers or they may have some
additional decoration or mangling. For example, some C compilers add an underscore at the
front of the source-code identifier, so a C function called foo will have the linkage symbol _foo.
The assertions must use the latter form, for example
subprogram "_foo" ... end "_foo";
12 Writing Assertions Bound-T for H8/300