Astrée comes with several real-life examples that demonstrate different analysis features and help you get started quickly.
The call graph of the analyzed application can now be viewed using the seamlessly integrated, award-winning aiSee graph viewer. The graph comprises statistical information about the distribution of alarms, and can be used for navigating the sources.
Code that has not been analyzed is always colored automatically in the editor.
Astrée now exports invariants at the end points of blocks and functions. The exported invariants can be displayed in the “Watch” window, and are now also displayed as tooltips in the editor.
The sorting of loop contexts in the “Watch” window has been improved. The contexts are now sorted in the order of loop iterations.
The “Summary” window now allows viewing alarms, errors, and coverage statistics per file, as well as alarms and errors grouped by categories. Double-clicking on a particular error takes you to the corresponding line in the source file.