Download Bound-T Reference Manual - Bound

+ 9 b = ?, c = ?
+ 10
The table above lists the ten steps in the control-flow graph of TempCon and shows the
arithmetic effect of each step. The effect is a list of assignments of the form cell = expression.
The cells are registers, flags or memory locations; their names depend on the target processor
and usually have no relation to the source-code variable names.
In this example, the arithmetic effect of step 1 increments cell p, assigns the value of cell p to
the cell Loc1, and assigns the value 2 to the cell SH. All the assignments in one step are done in
parallel so that one first evaluates all the expressions using the original values of the cells and
then assigns the new values to the target cells. This means that step 1 assigns the original (nonincremented) value of p to Loc1, not the new, incremented value.
Some steps, here for example step 2, have no arithmetic effect. Often such steps model jump
instructions.
When some effect of a machine instruction is not modelled for some reason (too complex or
not interesting for the analysis) it is represented by a question mark '?' and considered to have
an unknown value. In this example, step 6 assigns an unknown value to cell r and step 9
assigns unknown values to the cells b and c.
Reachable steps are shown by '+' signs and unreachable (infeasible) steps by '-' signs. In this
example, only step 3 is unreachable.
The detailed output for -show model continues with a table of the flow-graph edges:
Edge S -> T
+ 1 1 -> 2
- 2 2 -> 3
- 3 3 -> 4
+ 4 2 -> 4
+ 5 5 -> 6
+ 6 4 -> 5
+ 7 6 -> 7
+ 8 4 -> 7
+ 9 8 -> 9
+ 10 7 -> 8
+ 11 9 -> 10
Precondition
true
false
false
true
true
not ((a>b))
true
(a>b)
true
true
true
The above table lists the 11 edges between steps in the flow-graph for TempCon. Reachable
edges are marked '+' and unreachable (infeasible) edges are marked '-'.
For each edge, the column headed “S -> T” shows the numbers of the source step and the
target step. For example, edge number 8 goes from step number 4 to step number 7. A
comparison to the table of steps shows that the unreachable edges, edges 2 and 3, are
connected to the unreachable step 3, which is consistent. However, in general there may also
be unreachable edges between reachable steps.
For each edge, the column headed “Precondition” shows the logical condition that must hold if
the edge is taken (executed). The value “true” indicates an unconditional edge or an edge with
an unknown precondition and “false” indicates a false precondition which is the same as an
unreachable edge. Otherwise, the precondition is a relation between arithmetic expressions
composed of cell values. For example, after executing step 4, the target program can take edge
8 only if the value of cell a is greater than the value of cell b at this time.
Note that the precondition is only a necessary condition for taking the edge, but it may not be
a sufficient one. Thus, a “true” precondition does not mean that the edge is always taken; it
means that the edge can always be taken, as far as the analysis knows.
82
Understanding Bound-T Outputs
Bound-T Reference Manual