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, such as:
    • __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 imple­menting 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.

Affected old directive New analyzer-intrinsic function
__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.

MISRA-C:2004

  • 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.

MISRA-C:2012

  • 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}">
    <file>${VAR}.c</file>
  </files>
</dax>
  • 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">
  <options>
    <rulechecks>yes</rulechecks>
  </options>

  <rulechecks>
      <checks enable="all">
          <array-index>no</array-index>
      </checks>
      <rules enable="none">
        <M04>yes</M04>
        <M04.12.1>no</M04.12>
      </rules>
    </rulechecks>
</dax>
    Additional values can be passed where needed using the following syntax: 
    <dax version="1.1">
  <rulechecks>
    <rules enable="none">
      <M2012.6.1 value="char;int">yes</M2012.6.1>
    </rules>
  </rulechecks>
</dax>
  • 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">
    <bitfield_sign>signed</bitfield_sign>
  </abi>
</dax>
    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"
             reference="reference.aalref"/>
    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.

Updates to the TargetLink coupling

TargetLink logo
  • 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 “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 func­tion call) rather than 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 is now 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.

Configuration

  • 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 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.

Output

  • 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, or
    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.

Precision

  • 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.

Directives

  • 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: 
    __ASTREE_alarm((raise_at_caller;
                invalid_usage_of_os_service;
               "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;
    f(pa);
}

  • 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.