Astrée Release 15.04

* The C stub library now supports 16-bit and 32-bit architectures.
  The correct configuration is inferred from the size of a pointer
  in the ABI settings.
* When opening for the first time an analysis created with an older release,
  verify your local settings (Preprocessing, Reports, Code generators).
  In rare cases, the automatic conversion may produce invalid entries.

* The analyzer now computes significantly more precise intervals
  for expressions using the bitwise operators AND (&), OR (|),
  and XOR (^).
* The new option "partition-pt1" partitions first order lag (PT1) elements
  of the form "x + (i - x) * c" to allow for a more precise analysis.
  This option is enabled by default.
* The new non-relational domain of congruence intervals adds precision
  when dealing with deeply nested structures and arrays. It is activated
  via the new option "congruence-intervals=yes".
* The new option "exclude-signed-in-unsigned-overflows=yes" keeps precise
  information for signed values that are explicitly cast to unsigned.
  When casting the unsigned result back to signed, the analysis can then
  yield a more precise result. The analyzer reports overflows of signed
  values in unsigned computations only if the overflow also occurs
  in the signed representation. This feature is particularly useful
  for analyzing TargetLink-generated code.
  In addition, the new option "exclude-signed-negation-overflows-in-cto=yes"
  will exclude alarms raised by signed negations (when negating the smallest
  representable integer of a given type) when that negation occurs after
  casting an unsigned with CTO semantics.

C language features
* Added support for compound literals like "&((struct s){0})".
* Astrée now accepts non-standard empty initializer lists
 (e.g. "int arr[] = {};") which are supported by many C compilers.
* Added support for the keyword "typeof" (GCC extension).
  Astrée can now analyze code such as

    int x = 3; typeof(x) y = 900 / x;

* The new option "anonymous-global-structs-and-unions=yes" enables support
  for global anonymous structs and unions. This is a C language extension
  supported by some compilers. Astrée implements the behavior
  of the IAR compiler and names such objects after their first field
  with the prefix "_A_".
* The analyzer now accepts functions with variable argument lists.

* New:
  * "__ASTREE_trash" for use in stub functions (e.g. the C library stubs).
    It models a random modification of a given number of bytes of memory
    starting from a given address.
  * "__ASTREE_access((v, s));" models a read access on the first s bytes
    of the variable v.
  * "__ASTREE_huge_valf()" and "__ASTREE_huge_val()" return
    positive infinity as a floating constant of type float
    or double, respectively. They are used to implement
    the standard macros "HUGE_VAL", "HUGE_VALF", and "INFINITY"
    in the C stub library.
  * "__ASTREE_va_start((param));" allows implementing the "va_start"
    macro of the C standard library for initializing a "va_list" object
    to handle variable argument lists. An implementation of the macro
   (together with corresponding declarations of the "va_arg", "va_copy",
    and "va_end" macros) can be found in the standard C library stubs
    that are installed with Astrée.
  * "__ASTREE_malloc" can be used to implement "malloc", "realloc",
    and "free". Stubs for these functions have been added to the Astrée
    C library to illustrate the usage of the new directive.

* Improved and extended:
  * The "__ASTREE_comment" directive now accepts new types of comments
    for alarms. In addition to "false", "true" or "undecided", an alarm
    message can now also be classified as "true_high", "true_low"
    or "true_no_defect".
  * The directive "__ASTREE_absolute_address" has been extended
    to also work for static variables.
  * The analyzer now accepts "__ASTREE_partition_control" directives
    before for-loops with declarations, e.g.

      __ASTREE_partition_control((12)) for (int i = 0; i < 12; i++)

  * It is now possible to keep the partitions created during a function call
    after the return point. To that end, the function call should be preceded
    by the directive "__ASTREE_partition_control", e.g.

      __ASTREE_partition_control f(4);

  * Generalized the "__ASTREE_modify" directive to allow modifying
    lists of values and specifying new ranges for modified values.
    For example, the annotation

      __ASTREE_modify(( x, y[0-3], z->p; [11,42] ));

    sets the value range of x, y[0], y[1], y[2], y[3], and z->p
    to the interval [11,42].

    Note that this extended directive can raise a new kind of alarm
    if the specified interval is invalid.

* The new option "ais-export=yes" enables the collection of information
  about calls via function pointers. The collected information can be
  exported into an AIS file for use by a³ binary-level static analyzers
 (e.g. StackAnalyzer).
* Removed the option "show-hints".
* Removed the option "stop-parse-error-delayed" which allowed starting
  the analysis even if there were parse errors in the preprocessed files.
  All preprocessed files in the project must now either be accepted
  by the analyzer or removed.
* Added a new option "list-entry-functions=n" for collecting all functions
  with the maximum call depth of n. The collected information is used
  to display a list of potential entry functions for the analysis.
* The option "separate-function" is now fully compatible
  with the data flow options "dump-dataflow" and "report-shared-variables".
* There are two new ABI settings, "rounding_mode"
  and "rounding_mode_for_constants". The latter is used for the parsing
  of constants and the former is used for all other floating-point operations.
  Both optons can be set to "to_nearest" or to "all". The latter means
  that no assumption is made by the analyzer concerning the rounding mode.
  The default rounding mode for constants is "to_nearest" (as required
  by the C standard), while for the other operations it is "all".
  For architectures using internal representations with more than
  64 bits for doubles, "rounding_mode" should always be set to "all"
  since the double rounding is not equivalent to rounding to nearest.
* Replaced the option "warn-on-initializer-ranges=yes"
  by the new option "exclude-overflows-in-initializers=no".
* Removed the option "honor-cto-comments" for suppressing alarms
  in expressions marked with TargetLink's CTO comments. It is
  no longer needed since the analyzer can now auto­matically exclude
  the undesired alarms by semantics-based reasoning activated via
  the new option "exclude-signed-in-unsigned-overflows".

* Fixed the clock domain which could cause very high analysis times
  in release 14.10 and release 14.10i with build numbers below 234645.
* Fixed analyzer crashes when dealing with variables
  allocated to the absolute address 0.

Rule Checker
* Added support for the Misra-C:2012 rule set.
* MISRA-C:2004:
  * Added support for rules 3.4, 5.7, 12.1, 12.6,
    16.7, 19.3, 19.7, 19.9, and 21.1.
  * Extended support for rule 16.8.
  * Fixed check missing-else for rule 14.10 of MISRA 2004.
    The rule checker no longer warns about single "if"
    statements without "else". MISRA requires a final
    "else" clause only for "if ... else if ..." cascades.
  * The checks rule 5.4 have been refined and now also take enum tags
    into account.
  * Fixed check for rule 8.12. The respective rule check is
    no longer restricted to header files.
  * Improved the precision of MISRA-C rule checking to remove
    false alarms for the checks include-syntax, plain-char-usage,
    and statement-sideeffect.
  * Fixed false alarms concerning violations of rule M.8.8 and M.10.1.
  * Extended the checks for rule 20.2 to declared identifiers.
* Added a second comment density code metric that follows the HIS definition.
* The Rule Checker can now also check naming conventions for variables,
  functions, macros, and user-defined types. Valid names can be specified
  via regular expressions. The feature is found in the new "Style rules"
  category in the options.
* The Qualification Support Kit package that validates the Rule Checker
  is no longer an add-on to the basic Astrée QSK that validates
  the run-time error analysis. The two QSKs are now separate and
  require separate qualification test runs.

* All-new Result Viewer for exploring all findings of the analyzer.
  It displays a list of alarms and errors which can be easily browsed,
  sorted, and filtered. A single click on a finding loads all relevant
  information, such as the source code with tooltips and the list
  of all relevant contexts. Each finding can be classified and
  commented by the reviewer. Available classifications are:
  * true error
  * true error with high priority
  * true error with low priority
  * true error that is not considered a defect in the software under analysis
  * false alarm
  * undecided
  The results of the review appear in the XML reports and summaries.
  It is not necessary to re-run the analysis.
* It is now possible to generate AAL annotations automatically
  by simply right-clicking into the code displayed in the editor
  and selecting "Generate Annotation" from the context menu.
  After specifying a directive to insert, Astrée automatically
  generates the AAL specification that places the directive
  at the selected position in the code. The analyzed code is not modified.
* Added a new display of potential entry functions (periodic
  tasks and initialization functions) based on a pre-analysis
  of the source code. The list is available via the Tools menu,
  and is also displayed automatically if no analysis entry point
  was specified. Relevant tasks and initialization functions can
  then be selected to configure the analysis. Collecting information
  about potential entry functions can be disabled via the new
  option "list-entry-functions".
* The new editor view mode preference (accessible via Project ->
  Preferences -> Editor) allows to change the default view
  for preprocessed code. Available choices are "Original source",
 "Preprocessed source", and "Split view" which displays the original
  and preprocessed sources side by side.
* Improved editor layout and performance when adding a large number
  of annotations to the exact same program point.
* In the Output view of the GUI, it is now possible to copy
  not only whole lines but also line parts.
* The extraction of AAL annotations from the source files can
  now be canceled using either the stop button in the menu bar or
  the "Stop extraction" button in the "Advanced" tab of the Annotations view.
* Importing an Astrée options file (via Project -> Import ->
  Options) now only affects options that are listed in the imported file.
  Other options are no longer reset to their default value.
* The "new project" wizard can now be skipped (added finish button).
* It is now possible to jump directly back to the last displayed
  editor view by clicking on the "Files" entry in the project side bar
  or pressing Alt+E.
* Modified the default behavior when loading a DAX specification
  that references a wrapper file and at the same time contains further tags
  in the "<wrapper>" section. In this case, Astrée no longer
  re-generates the wrapper automatically but uses the referenced ".cfg"
  file. Running a batch mode analysis with such a file behaves likewise.
* Fixed the actions "Select category", "Unselect category", "Select all",
 "Unselect all" in the context menu of the Rules options.
  This fixes a known issue from release 14.10.
* The Preferences dialog has been extended by a field for specifying
  a user name for authentication with the Astrée server.

Toolbox and Data Dictionary import
* Astrée now imports value range annotations from the Data Dictionary
  also for calibration variables of vector and matrix types,
  and for variables with the flag "volatile=off".
* Fixed an issue that prevented the usage of the AbsInt Toolbox
  with MATLAB versions older than 2013a (removed the usage of "strsplit").
* Improved the detection of available subsystems in the Toolbox.
  This fixes issues with missing stub functions for lookup and
  interpolation routines.
* Optimized annotations generated for TargetLink’s
  linear search interpolations.
* Added an option to the AbsInt Toolbox for running a user-defined
  MATLAB script, e.g. for generating additional AAL annotations,
  before starting the Astrée analysis.
* The DD import now also annotates ranges for array parameters.
* The DD import now also generates assertions for vector outputs.
* Bounds for scaled fixed point values are now always rounded
  to integer numbers. Rounding is downwards for lower bounds
  and upwards for upper bounds.
* Added a new option for adding the source files of the DSFxp library
  to an analysis.
* Improved generated directives for RTE-Frame variables.

* The server data directory name may now contain special characters
 (like é).
* The server now closes all open client connections
  when the data directory is changed via the server controller.

The Astrée documentation has been extended by a new manual
containing detailed compliance matrices for Astrée
regarding undefined/unspecified/implementation-defined behaviors
according to the C99 standard.

Last modified on 4 May 2015 by
Copyright 2015 AbsInt.
An HTML version of these release notes is available at