Astrée Release 17.04

Standalone RuleChecker
RuleChecker and Astrée can now be used separately. 
This is implemented as follows.

▲ The product "Astrée for C" is replaced by the framework "ał for C",
  which contains the two analyzers Astrée and RuleChecker. 
  This renaming affects:

  △ the installation packages
  △ the names of the client, server, and server-controller executables
  △ the names of Qualification Support Kits
  △ the report files

▲ Analysis projects can now be created in one of two modes:

  1. Astrée mode
     for finding runtime errors, with the usual powerful user interface, 
     optionally invoking RuleChecker if you wish
  2. RuleChecker mode
     for finding violations of coding rules and compiling code metrics,
     with a simplified GUI, without running Astrée

  Note that invoking RuleChecker in the Astrée mode 
  maximizes precision on semantical rules.

▲ License files for previous Astrée releases are incompatible 
  with this release. All customers with active support have been emailed 
  new license files. Contact with any questions.

▲ The release notes for RuleChecker are now published separately as well. 

Improved performance
▲ Reduced analysis time for do-while loops.
▲ Reduced memory consumption when analyzing code with many function calls.
▲ Optimized GUI performance on huge analysis projects.
▲ Improved performance when loading very large projects on Windows.
▲ Reduced memory consumption during preprocessing, in both GUI and batch mode.

Improved precision
Improved precision for:

▲ strict comparisons on floating point variables in the octagon domain
▲ analyses with the option warn-on-field-overflows enabled
▲ evaluating comparisons between overflowing pointer expressions and NULL
▲ the Gauge domain for loops, enabled by the option gauges=yes. 
  For example, given the loop

    for (unsigned K=30, N=15; INPUT < K/2; K-=2)
  it can now prove that the loop terminates and thus N and K cannot overflow 
  if the float variable INPUT is known to be larger than or equal to 1.0.

General improvements
▲ When subtracting two pointers to different memory blocks and one of them 
  is the NULL pointer, the analyzer now warns about both issues in a single, 
  unified alarm message. Here is an example for subtracting a pointer pointing 
  to a variable x from the NULL pointer:

    ALARM (A): subtracting pointers on different 
               memory blocks { NULL } and { x }

▲ The analyzer now also detects misaligned memory accesses on variables which
  are known to be intentionally allocated to misaligned absolute addresses.
  Assuming that the char array a is allocated to the address 1001, Astrée 
  will detect that *(unsigned short*)(a + 3) accesses an aligned address 
  but *(unsigned short*)(a + 2) does not. For the latter, it now produces 
  the following alarm message:

    ALARM (A): invalid dereference: misaligned memory access at 1001 + 2 
               may not be a multiple of 2

▲ Accesses to address 0 no longer stop the analyzer with an error if 0 
  is explicitly declared as a valid absolute address:

    __ASTREE_absolute_address((int, 0));

▲ Optimized the analyzer to more precisely determine floating point bounds 
  close to 1e50.

▲ Improved the notifications about ambiguities due to side effects 
  in expressions. They are now more precise for assignments of the form 
  lhs = f(..) where lhs has no read accesses and f(..) is a function call.

▲ Invalid array size expressions (with a constant value ≤ zero) 
  no longer cause the analyzer to stop with an error message. Instead 
  all such arrays are assumed to be of size zero. The diagnostic rule A.1.2
  detects and reports such invalid array definitions.

▲ When ignoring the return value of a function by (incorrectly) assuming
  a void return type, the analyzer no longer stops with a definite 
  runtime error. Instead, the error is reported and the analysis continues
  with the assumption that the return value of the function is ignored.

▲ The analyzer no longer stops with a definite runtime error 
  in function calls that assume a non-pointer return value although 
  the called function has return type void. Instead, the error is reported
  and the analysis continues with the assumption that the return value 
  is not initialized and contains arbitrary values.

▲ Fixed false alarms about "Reinterpreting incompatible parameter type 
  in a function call" in function calls using a plain char type but expecting 
  an explicitly (un)signed char type, and vice versa.

▲ The octagon abstract domain is now used to:

  △ show the absence of division by zero over floats
  △ the absence of overflows in memcpy, bzero,
    and array accesses through pointers (as in p[i] where p is a pointer)

▲ Fixed the interpretation of character constants with values > 127
  in case of using the ABI settings char_sign=yes and bits_of_char=16.

▲ Astrée now supports the explicit allocation of variables into existing 
  memory blocks using absolute address directives. In such cases, it also 
  supports expressions that access several adjacent variables:

    unsigned char a, b;
    /* allocate memory for a and b */
    __ASTREE_absolute_address((char[2], 0x150)); 
    /* allocate a into existing memory block */
    __ASTREE_absolute_address((a, 0x150));     
    /* allocate b into existing memory block */
    __ASTREE_absolute_address((b, 0x151));
    unsigned short f(void) { 
      return *(unsigned short*)&a;   /* Read both a and b */ 
▲ Multiple declared variables with incompatible types are now 
  initialized consistently, independent of the parsing order of files. 
  Note that such declarations constitute constraint violations 
  and violate the diagnostic rule A.1.1.

Qualification Support Kits
▲ 13 additional test cases for Astrée
  and 26 additional test cases for RuleChecker.
▲ Consistency checks for XML result and XML report files.

C frontend
▲ Fixed an issue that could cause the frontend to abort with error 
  when enabling the option anonymous-global-structs-and-unions.
▲ The C frontend no longer prints unjustified warnings about type 
  incompatibility for variably modified array types when mixed with 
  constant size array type.
    int a[10];
    int n = sizeof(a) / sizeof(*a);
    int (*q)[n] = &a; /* this line no longer triggers a warning */
▲ Global __asm and __asm__ statements are now also handled automatically. 
  It is no longer necessary to define parser filters to remove such statements 
  from the code.
▲ The frontend now accepts differences of address constants with 
  the same base in integer constant expressions, e.g. &g[1] - &g[0]. 
  Such expressions, which are supported by some compilers, are still reported 
  as violations of MISRA-C:2004 rule 1.1 and MISRA-C:2012 rule 1.2.
▲ The frontend now accepts parameters with variably modified type, e.g. 
  int f(unsigned x, int (*p)[x])
▲ Shortened error messages about incompatible types 
  if the types involve structures.
▲ Function filters now only match whole identifiers. 
  Thus the feature now behaves exactly as documented.

Original-source frontend
▲ The analyzer no longer issues unjustified warnings 
  if the ## operator is followed by an empty macro parameter.
▲ Consistent handling of repeated expansions of a macro M defined as

    #define M N
    #define N() some_expansion

New project wizard
The wizard now simplifies the setup of analysis projects in all the different 
modes: Astrée, RuleChecker, and Astrée + RuleChecker.

Preprocessor view
▲ You can now preprocess a subset of the original source files 
  by selecting them and using the context menu.
▲ Likewise, you can select a source file and use the context menu 
  to exclude the corresponding preprocessed file from the project coverage.

Editor view
A line with more than one finding is now marked by a special icon. 
The number of findings is shown when hovering over it.

Findings view
▲ Lines from this view can now be copied to the clipboard.

▲ The Home and End keys now let you jump to the first or last 
  entry in the findings table.
▲ Double-clicking on the Comment column for rule violations 
  lets you comment on them in the original source code.

Overview → Filter view
▲ Added a button for resetting the filter to its default settings.

▲ The layout of the widgets can now be changed between horizontal and vertical 
  via a button in the toolbar.
▲ New Findings/Classification tab that lists the number of reported alarms 
  for each file and function together with their classification (uncommented, 
  undecided, true or false).

Analyzer → ABI view
Fixed the "Reset to analyzer defaults" action which in some cases would not correctly 
reset the ABI settings.

Analyzer → Options view
Reorganized the options to clarify which ones affect both Astrée and RuleChecker, 
and which affect only one of them.

Parser view
▲ Identifiers and regular expressions specified in the "Patterns 
  to ignore" tab now accept an optional replacement text. If specified, 
  matching patterns are replaced by this text instead of just being filtered.
▲ Entries in the list of "Patterns to ignore" can now be disabled 
  from the context menu.

Analysis history and differences viewer
▲ New dialog for providing a description when creating a new revision.

▲ Descriptions of leaf revisions can now be edited from the history tree.

▲ Fixed an issue that under Windows could lead to some revisions missing
  in the Differences viewer.

DAX export/import
▲ Improved the DAX export of nested preprocessor configurations 
  with relative base directories.
▲ The DAX export of the GUI no longer exports the output directories 
  of the Preprocessor view to increase the compatibility of DAX files 
  exported on other machines.

The identifier search now allows searching for struct/union member declarations 
and distinguishes between member reads, writes, taking the address of a member, 
and using it in a directive.

The dialog for starting the program slicer now allows selecting a variable 
that is written in the current expression.

Control Flow view
This new view displays the function calls in each process.

Data Flow view
▲ When using the Data flow view in the output area to investigate 
  data races, the context-menu function "Display findings" now narrows down
  the relevant findings not only to a certain variable but also to 
  a certain function in which the variable is accessed.
▲ The Data Flow view in the output area now also displays the location
  of each access to each variable for all processes under which the access 
  may occur.

Overview → Data Flow view
For each variable, this view now also displays the number of distinct locations 
at which it is read or written.

Overview → Filter view
This view affects the information displayed in Overview → Data Flow.

Call Graph view
The call graph view now also allows searching for arbitrary substrings 
of function names.

Watch view
Fixed cases of missing invariants for statements.

Annotations view
▲ Added a horizontal scrollbar when annotations exceed the available space.

▲ When Astrée reports alarms for a directive (e.g. an __ASTREE_assert) 
  that was introduced via an AAL annotation, it is now possible to invoke 
  the context menu on either the displayed directive in the code or 
  on the corresponding entry in the Annotations view, and select the new 
  action "Display findings", which then displays the list of alarms reported 
  for that directive.
▲ The Annotations view now also displays comments for annotations, e.g.:

    main { +1 statement} 
    insert before : __ASTREE_print(("start"); /*This is a comment.*/

Diagnostics messages formerly issued as errors or notifications (e.g. 
C constraint violations) are now covered by the new rule set "A. Diagnostics".
Make sure to enable this rule set for all Astrée analysis projects.

For old analysis projects specified in DAX, the new diagnostics can be enabled
by adding the following section to the DAX file:

    <rules enable="none">

Text report
▲ More compact tables for reached, not reached, and stubbed functions.
  The suffix "[at location]" at the end of each line is now omitted. 
 (The lines are still linked to the corresponding source code locations 
  in the GUI’s Output view.)

▲ The wording of two lines in the summary section has changed to clarify 
  their meaning:
  △ "Alarms on code locations"   → "Code locations with alarms"
  △ "Alarms on memory locations" → "Memory locations with alarms"

▲ Code metrics are now included in the text report file:

   /* Project metrics */
   | Project metrics |
   | RPATH       | 0 |
   /* File metrics */
   | File metrics   | CDFILE | LINE | FUN | PLINE |
   | src/Func1.c    |   0.00 |   19 |   1 |    16 |
   | src/Func2.c    |   0.00 |   34 |   1 |    31 |
   | src/Func3.c    |   0.00 |   13 |   1 |     8 |
   /* Function metrics */
   | Func1            |    2 |      2 |    0 |    7 |     2 |    13 |     2 |    2 |     0 |       2 |   1.94 |  0.00 |
   | Func2            |    6 |      3 |    0 |   16 |     2 |    28 |     3 |   18 |     2 |       1 |   2.31 |  0.00 |
   | Func3            |    2 |      2 |    0 |    5 |     1 |     5 |     2 |    2 |     0 |       1 |   1.62 |  0.00 |

▲ The Compressed Report file is no longer available.

XML report
The XML report file now also contains code metrics, if the option metrics=yes
was enabled for the analysis.

Custom reports
▲ In addition to HTML, the reports can now also be output as plain text 
  or CSV. The output format is specified in DAX via the new attribute 
▲ The Metrics View and the Metrics section in the configurable report 
  no longer list functions for which no metrics are computed by the analyzer 
 (e.g. unused static functions).
▲ Modified default headers for some sections in the configurable reports 
  to clarify their meaning.
▲ The files filter for custom reports now also affects the information 
  listed in the Data Flow section.
▲ The Data Flow section now shows the location of each access to each variable 
  for all processes under which the access may occur.
▲ It is now possible to specify the column to sort 
  the Data Flow information by.
▲ Custom reports may now contain information about the function calls in each 
  process as displayed in the new Control Flow view of the GUI.

▲ The former Summary reports have been replaced by predefined custom reports. 
  Summary report files specified in DAX version 1.3 or earlier are 
  automatically converted into the corresponding new custom reports. 
  The Summary Overview report file is no longer available.
▲ New variables for use in report headers and file names:

  △ %USER%
  △ %BUILD%
  △ %MODE%

▲ Improved the reporting of data races in the custom reports.

▲ The file filter in the custom-report configuration now also affects 
  the data race section so that only data races in the selected files 
  are listed.
▲ The report configuration can be included in the report, 
  either by including the whole configuration or by referring 
  to the configuration name.
▲ Added optional number of reported alarms for each file/function 
  in the project together with their classification.

Extensions of the DAX format
▲ New DAX version 1.4.

▲ The new project modes can be specified inside the <dax/> tag:

    <dax mode="rulechecker" version="1.4"> ... </dax>
    <dax mode="astree" version="1.4"> ... </dax>
  If not specified, the mode defaults to "astree".

▲ Modified attributes of the <parser-ignore/> tag:
  △ the file attribute used to import .par files from older Astrée versions 
    is no longer available
  △ it is now possible to specify a replacement 
    using the new attribute "replacement"

▲ In the custom report configuration, the tags that can appear 
  inside the <findings/> tag have been renamed as follows:

     DAX 1.3              DAX 1.4

    <alarms/>             <include-alarms/>
    <errors/>             <include-errors/>
    <notifications/>      <include-notifications/>

▲ DAX files referenced by the import attribute of the <abi/> tag 
  are now allowed to import an ABI from yet another DAX file.

▲ An entry in the <patterns-ignore/> section is now ignored 
  if it contains the new attribute enabled="no".

▲ The attribute coverage-ignore="yes" for <file/> tags 
  in the <preprocess/> section allows to exclude the corresponding 
  preprocessed file from the project coverage.

▲ The new tag <include-configuration mode="contents"|"name"/> 
  controls the inclusion of the report configuration in custom reports.

▲ The new key <alarm-classification> in the custom report configuration 
  controls the output of the number of reported alarms for each file/function 
  in the project together with their classification.

Preset option profiles
You can now pick from several option profiles to automatically set 
the most appropriate options accordingly. The following profiles are available:

▲ Setup (fast)
▲ Setup (normal)
▲ Analysis (fast)
▲ Analysis (medium)
▲ Analysis (normal)

The Setup profiles are a good choice for initial analysis runs to help you 
check and complete the setup. The Analysis profiles can then be used 
for final analysis runs, with different levels of precision.

New options
▲ generate-undeclared-absolute-addresses

  With this option enabled, accessing an undeclared absolute address will raise
  an alarm but the analysis will continue assuming that the address is valid. 
  Once the analysis has finished, suggestions for __ASTREE_absolute_address 
  directives will be displayed in the Output view. This corresponds to 
  the analyzer’s behavior in release 16.10.
  With the option disabled, the analysis stops for the current context 
  when accessing an undeclared absolute address. This corresponds to 
  the analyzer’s behavior in all releases before 16.10.
  The suggested workflow is to set this option during analysis setup, 
  review the generated directives, copy them into the "wrapper and stubs" file,
  and disable the option for subsequent analysis runs.
▲ separate-with-caller-stack-pointers
  enables a context-insensitive analysis of functions that access pointers
  to the caller stack.

▲ auto-unroll-size
  controls the maximum number of statements of loops that can be subject to
  heuristic loop unrolling (auto-unroll). The default value is 10.

▲ assume-unknown-pointers-are-valid
  triggers the following effects when enabled:

  △ The directive __ASTREE_initialize applied to a local pointer variable
    changes an invalid pointer into a possibly valid pointer, so that 
    the analysis may proceed.
  △ When a stub is generated for a function returning a pointer value, 
    then that pointer is assumed to be possibly valid (as with global pointers).
  △ When no size is given for a global array, accessing the array 
    does not stop the analysis. The analyzer continues with the assumption 
    that the array may have any size.
  △ If the option global-initialization is disabled and a global pointer 
    is read without being first written to, the analysis does not stop. 
    Instead, an alarm is emitted and the analysis continues with the assumption
    that the pointer was either NULL or pointed to some unknown variable 
    not declared in the analyzed code. 

Changes to existing options
▲ auto-generate-stubs
  now also generates stubs for function pointer calls with unknown targets.
▲ partition-double-if
  has been optimized to no longer partition double if-sequences 
  when the branches of the if are too big or when the conditions 
  don’t test the same variable.
▲ partition-array-access
  now performs a less aggressive partitioning. In most cases this improves 
  the analysis performance with no noticeable loss of precision. 
  When desired, the old, more aggressive partitioning behavior can be 
  restored by using the new option aggressive-partition-array-access=yes.
▲ Optimized the heuristic for selecting functions to analyze 
  context-insensitively (separate-function=*). Analyses using 
  this heuristic can become faster and slightly less precise.
▲ The option global-initialization has two new sub-options 
  that offer better control over the zero initialization 
  of global objects without initializers:

  △ tentative-initialization 
    controls the initialization of global objects with only tentative 
    definitions (i.e. only declarations without initializer)
  △ extern-initialization
    controls the initial value of global objects without initializer 
    and only 'extern' declarations

  Disabling one of these options will cause the analyzer to assume 
  arbitrary initial values for such objects.
▲ The option ignored-source-files has been removed. Files to be checked 
  are now explicitly specified in the new RuleChecker configuration. 
  See also these release notes’ sections on DAX and rule checks.

▲ The directive __ASTREE_suppress now also accepts "rules_category" as type, 
  causing all rule checks to be suppressed for the specified code region.

▲ The min_size parameter of the __ASTREE_partition_ranges directive 
  has been replaced by a new size parameter with slightly different semantics. 
  The analyzer now tries to adjust all partitions to exactly the specified size.
  If the partitioned range cannot be exactly divided by size, remaining values 
  are collected in an additional partition with smaller size.
  Please note that the size parameter can still be overridden by the 
  max_partitions parameter. That is, if the partitioned range divided by size 
  results in a number of partitions that is larger than max_partitions, 
  the analyzer will limit the number of partitions to max_partitions. 
  All of these partitions have approximately the same size, thus effectively 
  ignoring the size parameter. The new semantics of the size parameter 
  is particularly useful if a value needs to be partitioned in even intervals.

▲ The arguments of __ASTREE_alarm are now checked more strictly 
  during parsing to give immediate feedback about configuration issues. 
  Here are two examples of new error messages for invalid arguments:
    Invalid directive (message argument missing or empty). 
    Directive is ignored at ...
    Invalid directive (message argument not allowed with rule checker alarm). 
    Directive is ignored at ...

▲ The directive __ASTREE_partition_ranges((...)); now accepts 
  arbitrary constant expressions for its size and max_partition arguments.

▲ If an __ASTREE_assert assertion fails in multiple partitioning contexts, 
  only the contexts in which it failed are now reported.

▲ Removed restriction on the maximum number of created partitions 
  when explicitly specifying a maximum using the max_partition option 
  of __ASTREE_partition_ranges.

▲ __ASTREE_global_assert may now also be placed inside of function code 
  and thus can be applied to block-scope variables (like function-local 
  automatic or static variables).

▲ For the option "Use paths relative to destination directory…", 
  the default has changed from no to yes. This results in more compact 
  and stable file paths for modified destination directories.
▲ In nested preprocessor configurations, child configurations with an empty 
  base directory now inherit the base directory of their parent.
▲ Fixed the import of preprocessed files which could fail when the GUI
  preference "Synchronize preprocessed files" was disabled.
▲ Preprocessing no longer issues warnings if the analyzed code redefines 
  standard C macros such as __STDC_VERSION__.

Stub libraries
▲ All defines in the OSEK stub library are now guarded and can be 
  overwritten by the user if needed. The OSEK main function can also 
  be disabled by a macro definition if it conflicts with a main function 
  in the analyzed code.

▲ For the C stub libraries wchar_t and wint_t, it is now possible 
  to override the types and related macros by defining the following macros 
  during preprocessing:


  These macros are expected to expand to the desired definition 
  of the wchar/wint type or macro, respectively.

▲ The built-in preprocessor now also takes into account 
  ABI values inherited from a reference target when specializing 
  the C stub library.

▲ The owner of an analysis project can now be changed 
  by the server administrator in the server controller.
▲ When deleting a user, projects that are marked private to that user 
  are also automatically deleted from the server.
▲ Fixed an issue that could lead to a reset of the current 
  analysis configuration when the client lost connection to the server 
  during a configuration transmit.

Integration with TargetLink
▲ The generation of Astrée report files can be disabled under Preferences 
  and via the M-script function SetStandardReports.
▲ For AUTOSAR projects, the initialization phase of the generated 
  analysis wrapper code now contains a call to Rte_Start.
▲ The Astrée Preference dialog allows to persistently store the setting 
  for the batch mode execution. The M-Script API function InvokeAstree() 
  optionally uses this stored setting if available.
▲ The AbsInt Toolbox allows to exclude TargetLink standard files 
 (simulation files and DSFxp library files) via the preferences dialog.

Bug fixes
▲ Fixed the Windows installer for the Astrée client such that it installs 
  the OIL file converter for OSEK even if no server is installed.
▲ Fixed segmentation faults during startup on Linux installations 
  that use glibc versions < 2.5.16.
▲ Fixed an issue with the option exclude-signed-in-unsigned-overflows 
  which in rare cases caused the analyzer to crash.
▲ Fixed an imprecision that in release 16.10 caused unreachable return 
  statements containing function calls to not be reported as unreachable.
▲ Removed false alarms about out-of-bound array accesses when accessing 
  arrays of unspecified size.
▲ Fixed rare cases of missing value tooltips for (sub)expressions.

▲ Fixed an issue that caused comments of AAL annotations blocks 
  not to be loaded. Here is an example of such a block:

    __ASTREE_annotation(( /* comment was not loaded and displayed */

Last updated on 12 April 2017 by
Copyright 2017 AbsInt.
An HTML version of these release notes is available at