Visualization of recursions
All-new Results Viewer
Improved Configurations view
The XTC launcher no longer closes if an analysis fails.
number_of_loopsfor 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
Xequals zero. With this extension it is possible to express that
R2becomes infeasible iff there is a path from
snippet <PP1> continuing <PP2>,...” annotation.
:Section_<start address>, enabling it to be used in annotations.
trapfor software interrupt annotations.
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).
mbarinstruction (stack analysis only).