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, with a simplified user interface, without running Astrée

    Note that invoking RuleChecker in the Astrée mode as opposed to the standalone 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. If you no longer have the email, contact support@absint.com.

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

Analysis precision has been improved 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)
N--;
    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 larger than 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;
__ASTREE_absolute_address((char[2], 0x150)); /* allocate memory for a and b */
__ASTREE_absolute_address((a, 0x150));       /* allocate a into existing memory block */
__ASTREE_absolute_address((b, 0x151));       /* allocate b into existing memory block */
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.

Known issue

When enabling the gauge domain, in rare cases the analyzer may underestimate the value ranges of certain variables. Make sure that the gauge domain is disabled (this is the default setting of the analyzer), or contact support@absint.com for details on scenarios that trigger the undesired behavior.

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

Search

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.

Slicing

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

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:

<rulechecks>
    <rules enable="none">
        <A>yes</A>
    </rules>
</rulechecks>

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 */
|------------------------------------------------------------------------------------------------------------------|
| Function metrics | CYCL | RETURN | GOTO | STMT | PARAM | MLINE | LEVEL | PATH | CALLS | CALLING | LSCOPE | CDFUN |
|------------------------------------------------------------------------------------------------------------------|
| 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 format=html|text|csv.
  • 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:
    • %REPORT_TYPE%
    • %FILE_TYPE%
    • %PROJECT%
    • %REVISION%
    • %USER%
    • %VERSION%
    • %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 as 
    <dax mode="rulechecker" version="1.4"> ... </dax>
    or 
    <dax mode="astree" version="1.4"> ... </dax>
    respectively. 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 release notes about DAX and rule checks.

Directives

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

Preprocessor

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

    • __ASTREE_WCHAR
    • __ASTREE_WINT
    • __ASTREE_WCHAR_MIN
    • __ASTREE_WCHAR_MAX
    • __ASTREE_WEOF

    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 ABI values inherited from a reference target into account when specializing the C stub library.

Server

  • 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

TargetLink logo
  • The generation of Astrée report files can be disabled in the Preferences dialog 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 */
  ...));

RuleChecker

The release notes for RuleChecker are now published separately.