Astrée Release 11.12 -------------------- New features ------------ * Reorganization of analysis options 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. * Analysis time statistics The GUI can now display analysis time statistics. The statistics are updated online during a running analysis. Thus, it becomes possible to identify hot-spot functions in long-running analyses. * Detection of field escapes 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. * Full text search The Search view now provides an alternative full text search over the entire project. * Automatic tuning hints Astrée can now emit hints what to do in case of an alarm. * Improved user manual An additional Quick Startup Guide now offers a simple introduction for novice users. * Qualification Support Kit A Qualification Support Kit (QSK) for Astrée is now available. Interface --------- * Individual source files can now be excluded from the computation of the total coverage. * Code that is removed by constant folding (with "simplify=yes") is now marked in the editor. * The parser-view feature "Identifiers to ignore" has been superceded by "Expressions to ignore" which accepts regular expressions. * The "Global directives" and "Analysis start" views have been merged into a new "Analysis entry" view. The new view features a full-fledged editor for editing wrapper and stub code. * Includes for the shipped C library stubs are only used for preprocessing when the option "Use stubs for the standard C library" is enabled. * The preprocessor now supports adding a directory with all its subdirectories to the include path with a single command. * Notifications from the analyzer regarding performance issues and semantic assumptions are no longer classified as warnings in order to avoid confusion with alarms (potential runtime errors). C frontend/parser ----------------- * Relaxed scoping rules to allow more valid C99 programs. * Added support for function declarations within functions. * The parser now accepts non-standard strings containing newline. * The frontend no longer stops on array declarations without size. All such arrays are reported and the analyzer only stops if such an array is actually used. * Astrée can now handle functions that are declared using the inline function specifier. * Astrée can now ignore assembly blocks marked by "#pragma asm/endasm". This feature can be controlled via the parser view of the GUI. Analyzer -------- * Improved precision of computations that explicitly check for NaN or infinity. * Added warnings about repeated volatile input directives for the same variable. * Digital filter domain now supports 1st order filters with non-constant filter parameters. * Improved precision of digital filter domain for second-order filters with real roots. * Taking the address of a string literal is now allowed. Options ------- * New option "dump-invariants-with-unroll=[yes|no]" which behaves like "dump-invariants" but outputs the joined invariants for unrollings and iterations with widening. * New option "dump-unused-suppress=[yes|no]" enables warnings about unused suppress or comment directives. * The option key "warn-undef-intializers" has been renamed into "warn-undef-functions". * New option "cache-iterates=N" for controlling the size of a loop invariant cache. Enabling the cache can lead to a significant speedup in the analysis of nested loops. Directives ---------- * Renamed the directive "__ASTREE_import_types(())" into "__ASTREE_import(())". The new directive can import global types, functions, and variables. * The directives "__ASTREE_comment(())" and "__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. * The directive "__ASTREE_initialize(())" can now also be used within function scope to eliminate false alarms about uninitialized variables. Server ------ * The server now writes a log file which eases the debugging of server configuration issues. * The tray icon for the server controller has been removed. * The server now accepts a new command line option --name for setting its name as seen by clients. ============================================================================== Last modified on 15 December 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.12/