Visualization of recursions |
All-new Results Viewer |
Improved Configurations view |
number_of_loops
functor;The XTC launcher no longer closes if an analysis fails.
number_of_loops
for use in expressions at any program point P
evaluating to the number of loops contained in the routine containing P.ROUTINE R1 CALLS TO R2 INCARNATES <X>;
” to catch indirect calls
from the call stack when the bound X
equals zero.
With this extension it is possible to express that R2
becomes infeasible iff there is a path from R1
to R2
.snippet <PP1> continuing <PP2>,...
” annotation.:Section_<start address>
,
enabling it to be used in annotations.trap
for software interrupt annotations.fmod
/frem
instructions.dbcc
with cc == true
(no branch, just a fall-through to the successor).loop "x" max 5;
loop "x" max 5 by default;
global loop iteration default max 5;
For 1. and 2., the bound provided by the user is intersected with the bound computed by the loop analysis. If the intersection is empty, the loop is marked infeasible and an error is issued. If the computed bound is detected as unsafe, it is silently discarded and the user annotation is taken instead, without any intersection. The report file contains information about how the final bound is derived (i.e. whether it is the result of a user annotation, auto-detection or both).
For 1., it no longer makes a difference if a constant term or an expression is used.
Type 3 annotations will be ignored during loop/value analysis and only applied during path analysis (no unrolling is done with this bound).
dbcc
and rte/rtr
instructions.mbar
instruction (stack analysis only).stwbrx
instruction.brev
and circ
.