Astrée Release 11.08 -------------------- New features ------------ * External directives Directives can now be separated from the source code. The new AAL annotation language allows to identify source code locations based on the program structure. * 64-bit integers 64-bit integer types are now fully supported by Astrée. * Gotos The restrictions on gotos have been removed. Astrée can now also analyze code that contains backward gotos. * Detection of uninitialized variables Astrée finds and reports read accesses to uninitialized variables. The corresponding alarms can be enabled and disabled by the option warn-on-uninitialized=[yes|no]. * Full-range warnings The analyzer can now produce warnings whenever a variable changes its value to full range. This feature is controlled by the new option warn-on-fullrange=[yes|no]. * Improved TargetLink support Astrée now takes into account TargetLink's /* CTO */ comments in order to improve the detection of compute-through-overflow computations and to reduce the number of false alarms in TargetLink-generated code. This feature is controlled by the new option honor-cto-comments=[yes|no]. Directives ---------- * The "__ASTREE_partition_control" directive now also works for switch statements. * The "__ASTREE_known_fact" directive has been generalized for pointers. * Alarms can be commented and classified as "true", "false", and "undecided" using the new "__ASTREE_comment" directive. * The "__ASTREE_loop_unroll" directive now also works for for-loops with variable declarations. * The new directive "__ASTREE_import_types" allows to import types from project source files into the Global directives view. This significantly simplifies specifying global directives. Options ------- * The new option "warn-volatile-ignore=[yes|no]" controls whether Astrée issues a warning whenever the C volatile keyword is ignored. The new option is disabled by default to avoid too many warnings. * The new option "quick-widening=[yes|no]" controls whether the analyzer may enter the quick widening mode. Server ------ * The user space and system space server modes have been integrated into a single server executable. * Server data directories are now locked. The locking prevents inconsistencies that could arise if running more than one server on the same data. * Server access can be restricted to a set of registered users. * Servers now announce their existence on the local network and can be found automatically by the Astrée GUI. Interface --------- * It is now possible to detach open editor views into separate windows. * Added launcher for managing multiple installed client and server versions. * All unanalyzed code is now listed in the Summary/F view. It is possible to step through that list to traverse all unanalyzed code fragments. * The current project name is now displayed in the title bar of the GUI. * Code that has been discarded by the frontend based on the settings in the Parser view is now marked light gray in the editor. Frontend/parser --------------- * Functions with code that uses non-standard syntax extensions or inline assembly can be completely ignored by the frontend. * The parser can now guess the types of unknown functions, thus simplifying the analysis of incomplete software projects. Reports ------- * Added two new XML reports in which alarms and errors are ordered by category or source file, respectively. * All XML reports list the analysis options and semantic hypotheses. Other ----- * Optimized the raw analyzer output to reduce disc-space and network-bandwidth requirements. * Improved precision of the analyzer when checking for division by zero. Bug fixes (already delivered with patches for release 11.04) ------------------------------------------------------------ * Fixed the handling of temporary data in the Astrée client (client reports "Unable to write to the temporary directory"). * Fixed inadvertent removal of required integer cast operators. * Fixed cases where the analyzer stopped unexpectedly when evaluating a condition. * Fixed missing updates of the Summary/C window in the output area of the GUI. * Corrected strcpy implementation in the example C stub library. ============================================================================== Last modified on 12 August 2011 by alex@absint.com. Copyright 2011 AbsInt. http://www.absint.com/ ============================================================================== An HTML version of these release notes is available at http://www.absint.com/releasenotes/astree/11.08/