Astrée release 10.08


  • Added full support for C file scope rules. It is now possible to analyze programs in which different global variables and types have identical names in different C source files.
  • Added support for line directives of the form “#line <num> <string>”.


  • The Astrée server can now be started as a Windows service, making it independent from user sessions.
  • Improved the synchronization of multiple clients that access the same analysis project on the same server.


  • New Astrée icon.
  • Increased speed and reduced memory consumption when handling large analyzer logs.
  • All long running operations can now be aborted by the user.
  • The preprocessed source code that is analyzed on the server can now be downloaded into a local directory on a client machine. The downloaded files can also be synchronized with the server files.
  • Astrée is now shipped with several pre-configured ABIs which can be loaded in the “ABI” view.
  • Reorganization of the analysis results views:
    • Removed the separate views “Errors”, “Alarms”, and “Warnings”. This information can now be found under “Output”.
    • Display the call graph using the aiSee graph viewer. The graph can be used for navigating the sources. It also comprises statistical information about the distribution of alarms. See screenshot.
  • Reorganization of the Output area:
    • “Output” window renamed into “Log”.
    • Extended the “Summary” window. It is now possible to view alarms, errors, and coverage statistics per file, as well as alarms and errors grouped by categories. See screenshot.
    • Improved the precision of coverage information. Lines outside of functions are no longer taken into account.
    • Added a navigation panel to the “Log” and “Summary” windows, enabling easy navigation through alarms and errors.
    • Added a separate “Warnings” window which collects all warning messages.
    • Added new “Messages” window to display and navigate all analyzer messages for a code location that has been selected in the editor view.
  • Project browser:
    • Added new status area below the left-hand menu. It provides stats about the analysis results including errors, alarms, warnings, coverage, and analysis time. A traffic light summarizes the analysis stats, enabling a quick assessment of the analysis results. See screenshot.
  • Interactive result exploration:
    • Astrée now also exports invariants at the end points of blocks and functions. The exported invariants can be displayed in the “Watch” window.
    • Loop contexts in the “Watch” window are now sorted in the order of loop iterations.
    • Exported invariants are now also displayed as tooltips in the editor. The displayed invariants hold for all contexts. See screenshot.
  • Editor:
    • Non-analyzed code is always colored automatically. See screenshot.
    • Added syntax highlighting and auto-completion for analysis directives.