Astrée Release 15.10

Detection of data races and inconsistent locking
Astrée has been extended to perform a precise and sound analysis
of asynchronous programs. All possible interactions between parallel tasks
are now considered. All potential data races and lock/unlock problems
are detected. ARINC 653 and OSEK applications can be analyzed fully
auto­matically taking the OS behavior into account.

* New categories of alarms:
  * Data races
   (read/write or write/write concurrent accesses by two threads
    to the same memory location without proper mutex locking)
  * Inconsistent locking
   (lock/unlock problems)
  * Invalid calls to operating system services
   (e.g. OSEK calls to TerminateTask() on a task with unreleased resources)

* New OS stub libraries, fully integrated with the built-in preprocessor:
  * OSEK
  * ARINC 653

* New analyzer-intrinsic functions for modeling OS actions:
  * __astree_create_process
  * __astree_start_process
  * __astree_lock_mutex
  * __astree_unlock_mutex
  * and many more

* New analyzer options:
  * warn-on-data-race=[yes|no]
    warns about potential data races (enabled by default)
  * log-parallel-iter=[yes|no]
    prints extra progress information
    when iterating over asynchronous processes
  * dump-data-dictionary=[yes|no]
    prints the final ranges of global variables
    and statistics about shared memory usage
  * dump-process-dataflow=[yes|no] collects reads and writes
    of global variables and aggregates them per process

* Collection of data flow information per parallel process/task.
  The collected information is displayed in the GUI and can be
  written to a report file.

New analyzer-intrinsic functions
Several directives have been replaced by analyzer-intrinsic functions.
Semantically, they still correspond to directives, but are no longer listed
as such in the analyzer log.

This modification affects all built-in operations of the analyzer
that are used solely for implementing stub functions.
Existing source files for stubbing can still be used
when including the astree.h header file and defining
__ASTREE__ and __ASTREE_LEGACY_DIRECTIVES__ when preprocessing.

Here is the list of the affected directives and the new
analyzer-intrinsic functions they have been replaced with:

* __ASTREE_bzero        ->   __astree_bzero
* __ASTREE_double_exp_2 ->   __astree_double_exp_2
* __ASTREE_double_extract_exponent  ->  __astree_double_extract_exponent
* __ASTREE_double_sqrt  ->   __astree_double_sqrt
* __ASTREE_exit         ->   __astree_exit
* __ASTREE_huge_val     ->   __astree_huge_val
* __ASTREE_huge_valf    ->   __astree_huge_valf
* __ASTREE_huge_vall    ->   __astree_huge_vall
* __ASTREE_malloc       ->   __astree_malloc
* __ASTREE_memcpy       ->   __astree_memcpy
* __ASTREE_va_start     ->   __astree_va_start

The GUI offers automatic conversion of old directives via the Tools menu.

Rule checks
* For easier configuration and better understanding,
  all rules and checks have been merged into a single view.
  For each rule, you can now see all the checks used by it.
  When enabling or disabling some aspect of a rule by toggling
  a check, you immediately see which other rules are affected.
* The list of pre-defined filters in the Configuration view
  has been extended by the rule categories of MISRA C and
  MISRA AC AGC (Mandatory, Advisory, Obligatory, Readability,..).
* Header files are now only checked in contexts in which
  they are actually included while preprocessing. This fixes
  unjustified warnings about preprocessing problems in rule checking.

* Added support for rule 16.10.
* Improved precision for rule 13.6 to eliminate false alarms.
* For violations of 19.15, the analyzer now reports the exact line
  where a file is included twice.
* The check for rule 13.3 has been refined and now also takes several
  patterns of indirect equality tests into account.
* Improved precision to eliminate false alarms about violations of rule 8.9.
* Fixed rare false alarms for rule 19.15.
* Improved coverage of rule 18.4 by adding a check
  that warns about union objects.

* Added partial support for rule 8.13.
* Corrected check for rule 2.5. Macros defined in the preprocessor settings
  are no longer subject to the rule check "unused-macro".
* For violations of Dir. 4.10., the analyzer now reports
  the exact line where a file is included twice.
* Improved coverage of rule 19.2 by adding a check
  that warns about union objects.

Extensions of the DAX format
* Incremented the version number to 1.1.
* The elements "options", "abi", and "parser-ignore" now support
  importing settings from other DAX files. This is done using
  the optional "import=<file>" attribute.
* Model link settings for code generated via TargetLink
  or EmbeddedCoder can now be specified in DAX files.
* It is now possible to refer to environment variables in text nodes
  and attribute values of DAX files. Here is an example which evaluates
  two environment variables YES and VAR:

    <dax version="1.1">
      <files use-relative-paths="${YES}">

* Improved the rule checker configuration in DAX files.
  Instead of using the now-deprecated "rules" and "checks" options,
  they can now be specified in a new <rulechecks> section
  as shown in the example below:

    <dax version="1.1">

          <checks enable="all">
          <rules enable="none">

  Additional values can be passed where needed using the following syntax:

    <dax version="1.1">
        <rules enable="none">
          <M2012.6.1 value="char;int">yes</M2012.6.1>

* The ABI section now supports loading one of the predefined ABIs.
  Individual settings from this ABI can still be overwritten. Here is
  an example which loads the ABI for 32-bit Intel x86 but overrides
  the setting for sign of bitfield:

    <dax version="1.1">
      <abi target="ia32">

  If the target option is omitted, Astrée uses the analyzer
  default ABI settings that are specified in the user manual.

* The server-side reference file for inserting AAL annotations
  can now be exported via Annotations → Advanced and referenced
  in DAX files via the "reference" option of the <annotations>
  tag. Example:

    <annotations file="annotations.aal"

  Note that the reference file is specific to the version
  of the Astrée server and the operating system it is running under.
  It may need to be re-generated when uploading it to a server
  with a different version number or running under a different OS.

Integration with dSPACE TargetLink
* Added support for TargetLink 4.0.
* The Toolbox for TargetLink now also considers
  the IncludeFileSearchPath and SourceFileSearchPath properties
  of the data dictionary. Paths listed in IncludeFileSearchPath
  are added to the list of include paths for preprocessing,
  and C source files from paths listed in SourceFileSearchPath
  are added to the files to analyze.
* It is now possible to specify an additional script or executable
  for post-processing files generated by the "Import Data Dictionary".
  Post-processing is applied to the generated "Wrapper and stubs"
  as well as to the "Annotations" file. The script can be specified
  either in the Toolbox or in the "Code generators" view.
* The DD import now also generates directives for ranges
  of calibrateable struct components.
* Improved handling of interpolation routines.
* Added new configuration elements to specify top-level subsystems
  for which calls are generated in the analysis wrapper. This is useful
  if a subsystem’s code is called by a top-level subsystem (e.g.
  when using model referencing). The new configuration elements are
  "data_dictionary_toplevel_subsystems" in XTC, "<toplevel_subsystems>"
  in DAX, and "Code Generators" -> "Import Data Dictionary" in the GUI.
* The "MATLAB script" field in the Astrée preferences
  now also accepts MATLAB script code (e.g. a function call)
  instead of just the name of a MATLAB script file.

Options and ABI
* New options:

  * keep-float-specials
    configures the treatment of infinities and NaN. If disabled (default),
    the analyzer behaves like in previous releases, i.e. it warns about
    such values and discards them before continuing with the analysis.
    If the option is enabled, the analyzer omits such warnings and instead
    keeps the special values. This mode of operation is useful for modeling
    targets on which floating point special values do not raise exceptions,
    e.g. quiet instead of signaling NaN.

  * dynamic-smash-variables-threshold=n
    allows to specify a maximum number of variables to which a pointer
    may refer before those variables are smashed, i.e. represented
    by a single abstract object.

  * automatic-partition=[yes|no]
    controls all automatic partitioning heuristics. This option
    has no influence on user-defined partitioning directives,
    in contrast to the option "partition=[yes|no]".

  * warn-read-of-never-written-variables
    enables warnings about read accesses of global or static variables
    which have neither an explicit initializer nor a previous assignment.
    Such reads are reported as class D alarms.

  * --export <archive>
    batch mode option for exporting the analysis configuration and results
    as an .aaf archive at the end of the analysis run.

  * The alignment of char arrays can now be configured via the new ABI
    setting ">alignof_char_array". The default value is 1.

* The option "warn-on-uninitialized" has been deprecated.
  Warnings about accessing uninitialized variables with automatic storage
  duration (local variables) are now always enabled. Such accesses are
  reported as class A alarms.

  Uninitialized local variables have sometimes been used for generating
  full-range intervals in user-defined stub function, typically following
  this pattern:

    /* stub function: returns a random character */
    char random (void) { char c; return c; }

  This pattern will now always lead to a class A alarm.
  Stub functions of this kind should be rewritten as follows:

    char random (void)
    { char c; __ASTREE_modify((c; [-128, 127])); return c }

  The modify directive acts like an assignment that initializes
  the variable with the specified range. The C stub library that
  is shipped with the tool has been corrected in this manner.

* Fixed import of a partial list of rule checks from an options file
  so that already configured rules are no longer overwritten.

* The different kinds of analysis settings (options, ABI, etc.)
  can now be imported from and exported to the DAX format. Files
  with analysis settings in old formats (.opt, .abi, etc) can still
  be imported but are no longer exported by the GUI. For options
  and rules, the new DAX export allows either a full export of all
  options and rules or alternatively the export of only those options
  and rules that have been explicitly modified, i.e. that deviate
  from the tool's default settings.

* The views for the analyzer options, rule-checker options and ABI
  have been restructured and unified. The new view is available via
 "Analysis configuration" -> "Settings" in the project toolbar.
  It now provides the same look and feel for all configuration items
  and a filtering mechanism for faster lookup of specific options,
  rules, or ABI settings.
* The ABI configuration view now displays the target that has been
  selected from the list of predefined targets. Only explicit deviations
  from the selected target are highlighted.

Code browsing
* Functions defined in a preprocessed file can now be listed directly
  in the Files list in the main navigation panel. This enables
  easier and faster navigation of large files.
* The editor view now highlights matching parentheses and braces
  when positioning the cursor in front or behind such characters.
* The preprocessing view now distinguishes two modes of operation.
  By default, the view allows to configure and start the built-in
  preprocessor. When using an external preprocessor instead, the view
  can be switched into a new mode by unchecking the new option
  "Use the built-in preprocessor". In this mode you can enter
  the include paths and defines that were used by the external
  preprocessor. This information is then used for locating
  the original source files and for configuring the rule checking
  on those files.

Result Viewer
* More fine-grained filtering of the alarms to be displayed.
  The number of currently visible alarms is shown.
* The Viewer now lists unused comments, i.e. comments that no longer
  refer to alarms. Such comments typically come about when the code
  under analysis was modified before re-running the analysis. You can
  now move them to the corresponding alarms in the new analysis run,
  or delete them outright.
* It is now possible to comment alarms which are raised
  by directives (e.g. __ASTREE_assert) that have
  been inserted via AAL annotations.
* Comments imported via DAX in batch mode are now visible
  in the Result Viewer after a batch analysis.

* The output and report files no longer list all analyzer settings,
  but rather either:
  1. only the settings that deviate from the default,
     i.e. have been modified by the user in the GUI,
  2. only the settings that are listed in a .dax or .opt
     file when running the analysis in batch mode.
* When preprocessing files with the built-in preprocessor,
  the invocations of the preprocessor and its outputs are now part
  of the analysis log. They can be found in the "Output" tab of the GUI
  and the text report file.
* In the editor, the currently displayed tooltip can now be copied
  to the clipboard with Ctrl+T.
* The code metrics view and report have been extended by a Location column
  which holds the locations of functions for which the metrics are given.

* The new domain of distance to zero for floats allows for a more precise
  analysis when dividing by a float that can be positive or negative.
  It detects if the absolute value of such a variable is far enough
  from zero so that overflows can be excluded. This prevents some
  false alarms about floating-point divisions which were raised
  by previous versions of Astrée.
* Added a new interpolation domain for a more precise analysis of typical
  interpolation routines (e.g. as generated by the TargetLink code generator),
  resulting in fewer false alarms about potential run-time errors.
  The new domain can be enabled by the option "interpolation=yes".
* Improved the precision when logical expressions appear inside comparisons,
  such as in

    if((a < 0) == 0)

* Improved the precision of the analysis for possible ambiguities
  due to side effects in expressions.

* It is now possible to assign absolute addresses to variables
  with incomplete type as in the following example:

    unsigned char* rom[];
    unsigned char* rom_end[];
    __ASTREE_absolute_address((rom, 0x1000));
    __ASTREE_absolute_address((rom_end, 0x2000));
    size_t rom_size = rom_end - rom;

* New directive __ASTREE_alarm for raising alarms in stub functions.
  The directive can be used to raise any kind of alarm with a freely
  configurable message text. Moreover, the alarm can be optionally
  reported at the location where the stub function is called,
  rather than at the location where the directive is inserted.
  Here is an example from the new OSEK stub library:

                   "invalid call to ReleaseResource
                   (resource has not been acquired)"));

C frontend
* The analyzer now allows the linking of functions that are declared
  with incompatible types in different compilation units.
  Hence, the following AUTOSAR-compliant code can now be analyzed:

    /* file1.c */
    typedef int T;
    void f(T* p) { }

    /* file2.c */
    typedef int T[8];
    void f(T*);
    void main (void)
      int a;
      int* pa = &a;

* Flexible array members are now supported,
  i.e. types of the following kind are accepted:

    struct S {
    int a;
    int  b[];

* The analyzer now accepts empty struct declarations as extension,
  i.e. declarations of the following form are accepted:

    struct S {
    int a;
    ; /* empty struct declaration */
    int  b;

* Old GCC-style designated initializers are now accepted,
  e.g. { x: 42 }, which behaves the same as { .x = 42 }.

* The analyzer now handles more variants of GCC-style
  inline assembler automatically.

Libraries and stubbing
* The C stub library for Astrée now supports all
  ABI configurations that are supported by the analyzer.
  The built-in preprocessor automatically configures
  the library according to the specified ABI settings.
* Automatically generated stub functions are no longer considered
  for reached-code statistics as they are not actually part
  of the analyzed code.

Report files
* The types of alarm comments are now printed in a separate column
  in summary report files.
* XML summary report files can now link each alarm to the model link
  HTML file containing the source code for which the alarm was raised.
  This requires a proper configuration of the display of model link files
  via "Code generators" -> "Model link".
* Missing directories for report files are now created automatically
  if possible.

Other modifications and improvements
* Fixed a known issue from release 15.04 where importing projects
  created with release 14.04i, 14.10, or 14.10i would in rare cases
  crash the server.
* Fixed the printing of string constants when using the option
  "dump-source" or the scenario builder. This fixes another
  known issue from release 15.04.
* The analyzer now also warns about potential ambiguities due to
  side effects on function-local static variables.
* Fixed cases of missing and misclassified declarations when searching
  for identifiers in the Search tab of the GUI.

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