Astrée Release 10.12 -------------------- New preprocessor support ------------------------ It is now possible to specify a list of original source files and preprocessor settings (include paths and defines). The specified files can be automatically preprocessed and analyzed by Astrée using a built-in preprocessor. The installation also includes a sample C library implementation that uses Astrée directives for stubbing frequently used functions. New project wizard ------------------ When creating a new project, a wizard dialog guides the user through the basic analysis settings. The wizard also provides online help for each of the configured options. New call graph browser ---------------------- The new browser provides a better overview of the alarm distribution in the analyzed software. It allows to display only the relevant program parts and to investigate modules individually. New XML reports --------------- Analysis results can be exported in XML format. The XML reports comprise: * a summary of the analysis results; * a list of all error and alarm messages including location information in preprocessed and original source code; * detailed coverage information for all analyzed source files. The generated XML reports can be displayed in a web browser or imported into Microsoft Excel and Word using the included XSLT stylesheet. New batch mode option --files ----------------------------- When running in batch mode, the Astrée client recognizes the new option --files <file list> Before running the analyis, the list of files to be analyzed is updated to match the files given in <file list>. New directive __ASTREE_exit((expr)) ----------------------------------- This new directive enables implementing program exits that are not errors, e.g. calls to the exit(int) function. Exit codes are reported by the analyzer. Improved user handling ---------------------- Specifying a user name for a server connection is now mandatory. The default user “anonymous” can be used to create analyses without access restriction. User data and the local settings of analysis projects are now stored in the server working directory. As a consequence, the local settings of an analysis project are preserved when installing new versions of Astrée. Also, the local settings of one user at a certain client can now be transferred to another user at a different client (via export and import). Modified defaults ----------------- The default values for the options "volatile-global" and "volatile-auto" have changed. By default, the analyzer no longer assumes that the values of variables that are declared using the C keyword "volatile" may change asynchronously. The new default behavior matches the semantics of the keyword in most programs. Volatile behavior of individual variables or at certain program points can be expressed using Astrée directives. Faster server operations ------------------------ Adding/removing many files to/from a project works much faster. Improved coverage information ----------------------------- Coverage information is now computed as the percentage of analyzed statements rather than lines. The Summary window features a new column that displays the number of statements that have not been analyzed. Analyzer enhancements --------------------- * Computing pointers with negative offsets no longer causes false alarms. An alarm is only raised if a pointer with a negative offset is dereferenced. * The analyzer no longer stops when evaluating an array of function pointers that contains a pointer to a function with missing definition as long as no attempt is made to call the missing function. * In cases of recursive function calls, the analyzer now always stops with an unhandled-recursion error. Interface enhancements ---------------------- * The Log window can now display even very large analyzer outputs. Large projects are also loaded faster. * The displayed duration of the analysis now corresponds to the total time elapsed instead of the analysis time of the main function only. * In the Analysis Options views the options that differ from the defaults are highlighted. Tooltips show the default option values. * Arrays and structures in the Watch view are now displayed hierarchically. Type information is available at the uppermost and lowermost levels. * The Summary, Watch and Message windows now support filtering (press Ctrl+F). * The sorting order of messages in the Summary view has been reverted to match the user intuition. * All output area windows except the graph browser can now be fully navigated using only the keyboard. * The project file tree has been changed to a list to simplify navigating projects with deep hierarchies. Path information is displayed as a tooltip. * Modified projects can now be explicitly saved on the server (new Project menu entry). Enhanced configuration possibilities ------------------------------------ Several options for configuring the user interface have been added, including: * actions at client start (whether to start a local server); * actions at analysis start; * editor defaults and warnings. New file astree.h ----------------- The "share" directory of the installation contains a new header file "astree.h" with macros for stripping the Astrée directives during compilation. Bug fixes --------- * Fixed batch mode option --drop to properly delete projects from the server. * Fixed inconsistent line breaks in the Log window when running the analyzer on Windows. * Corrected rare problems concerning the loading of the original source code. * Fixed rare cases of unreachable code not being marked gray in the editor. * Corrected the behavior of the expert option "partition-all" when partitioning loops. * Corrected the naming of watch window columns when loading invariants. * Fixed error message about incompatible types. * Corrected issues with the constant propagation of enum values. * Fixed the global directives editor to accept tabulator characters. ============================================================================== Last modified on 15 December 2010 by alex@absint.com. Copyright 2010 AbsInt. http://www.absint.com/ ============================================================================== An HTML version of these release notes is available at http://www.absint.com/releasenotes/astree/10.12/