All analysis options are now available via a single options view in the GUI. The number of options has been reduced in order to simplify the setup.
The GUI can now display analysis time statistics. The statistics are updated on-line during a running analysis. Thus, it becomes possible to identify hot-spot functions in long-running analyses.
Astrée can track pointers that escape structure fields as long as the pointers stay in the same variable. While this behavior enables a low number of false alarms, it can sometimes be interesting to detect such field escapes. The new option warn-on-field-overflows=[yes|no] controls whether Astrée should report alarms in such cases.
The Search view now provides an alternative full text search over the entire project.
Astrée can now emit hints what to do in case of an alarm.
An additional Quick Startup Guide now offers a simple introduction for novice users.
A Qualification Support Kit (QSK) for Astrée is now available.
simplify=yes) is now marked in the editor.
#pragma asm/endasm. This feature can be controlled via the parser view of the GUI.
dump-invariants-with-unroll=[yes|no]which behaves like
dump-invariantsbut outputs the joined invariants for unrollings and iterations with widening.
dump-unused-suppress=[yes|no]enables warnings about unused
warn-undef-intializershas been renamed into
cache-iterates=Nfor controlling the size of a loop invariant cache. Enabling the cache can lead to a significant speedup in the analysis of nested loops.
__ASTREE_import(()). The new directive can import global types, functions, and variables.
__ASTREE_suppress(())can now be inserted with relative scopes using the annotation language AAL. Alarms can therefore be commented or suppressed depending on their location in the code structure.
__ASTREE_initialize(())can now also be used within function scope to eliminate false alarms about uninitialized variables.
--namefor setting its name as seen by clients.