Astrée release 17.10

New comment mode

Alarms reported by Astrée can now be commented on using code patterns rather than AAL annotations. While the latter are more precise (as they identify code locations unambiguously), code patterns can be very useful for keeping track of alarm comments in projects with significant code changes between analyzed revisions, notably when using code generators.

The default commenting mode for new projects can be set under Project → Preferences → General → Findings.

For existing projects, the default mode is AAL. It can be changed, but any existing comments need to be transferred manually.

Faster performance

  • The analyzer is now substantially faster by default. In some cases this can lead to less precise results. To reset precision to previous levels, use the new option widening-with-thresholds=yes.
  • The integrated preprocessor now performs better as well.

Higher precision

  • The analysis is now more precise for expressions that involve arrays and occur inside of loops.
  • Improved the precision of the octagon operations on divisions. Operations such as x/y when 0 < x < y are now inferred to be smaller than 1.
  • Improved the heuristics for double if partitioning and increased the threshold for aggressive array index partitioning. This modification fixes precision regressions that have been observed on certain code with release 17.04.
  • Optimized the loop caching heuristic (controlled by the option cache-iterates) to make better choices when selecting loops for caching. This may increase analysis precision as well as reduce memory consumption.

Other improvements

  • The tick character ' can now be used in filter patterns and replacements.
  • The notifications about ambiguities due to side effects in expressions or initializers, and the option warn-sideeffects that controlled such notifications, have been removed. They are replaced by the two diagnostic rules A.4.1 and A.4.2 and their respective checks evaluation-order and evaluation-order-initializer.
  • When starting a client using alauncher, a temporary server can be started in the background using the new option --temp-server. The client automatically connects to that server and the server is shut down when the client process stops.

Qualification Support Kits

  • Under Windows, the maximum path length limitation is now checked every time a test case is loaded.
  • Four test cases have been added:
    • qk_aal_comment_annotation_alarm
    • qk_option_max_finite_int_set_size
    • qk_option_warn_on_subsequent_uninitialized_reads
    • qk_option_widening_with_thresholds
  • The test case qk_option_warn_sideeffects has been removed, as it is now covered by new test cases in the RuleChecker QSK.

Windows support

Since release 16.10, Astrée relies on DLLs from the Microsoft Visual C++ Redistributable for Visual Studio 2017. Starting with this release, the redistributable is included in the installer as an optional component, or can be installed manually at a later point from the directory share/3rdparty/vc.

C frontend

  • Added support for:
    • GCC’s __alignof__ and the C11 feature _Alignof
    • the C11 feature _Static_assert
    • constant expressions in array member designators of offsetof()
  • The frontend now prints an error message when __ASTREE_trash or __ASTREE_access are accidentally used with a non-pointer variable.
  • The frontend now accepts multi-character character constants and handles them like GCC, i.e. as digits to the base UCHAR_MAX+1.
  • The frontend now allows sizeof(*x) when *x has type void. The result of this operation is 1, which corresponds to how GCC behaves.
  • Modified the way in which static variables and functions are renamed by the analyzer to resolve naming collisions when linking translation units into a global program representation. The new renaming scheme uses much shorter, and more stable, names.
    A static function or variable X may now be renamed into 
    __ASTREE_static_X_8
    where 8 is a stable ID for the file in which X is defined. Previous versions of Astrée used to rename X into something like 
    X__ASTREE_drive_C_users_john_doe_analysis_tmp_fileX_c_3487463
  • Inline functions with external linkage are now represented by a single definition.
  • The frontend now retains type qualifiers when using typeof (GCC extension). This modification can affect rule checking on typeof expressions involving qualified types.
  • The tool now also notifies about ambiguities due to side effects in expressions or initializers whenever an object is modified multiple times between two sequence points.
  • Fixed the concatenation of two string literals in the case that the first string literal ends in an escape sequence.
  • Fixed the parser filter for the case of applying several filters to immediately adjacent characters.
  • Fixed handling of source files with inconsistent line endings.

Original-source frontend

  • Suppress and comment directives in source file comments now also support negative offset/length values.
  • Fixed the parser for original source files to allow the character sequence ?\ inside of string literals.

Project bar

  • File lists can now be filtered by pressing Ctrl+F.
  • The new Information view displays general project information such as name, type, and revision.
  • The Welcome view is no longer accessible from here. It only opens on startup and can later be accessed via the Help menu.

ABI configuration view

Corrected cases when the ABI values pointer_attributes_1, pointer_attributes_2, and pointer_attributes_3 were not reset.

Rules configuration view

  • After importing RuleChecker configurations, the configuration list in the Rules tab now automatically expands with the most recently imported configuration selected.
  • Reorganized the context menu in the Rules configuration view to improve usability.

Preprocessor view

  • Improved the display of the preprocessor output.
  • The automatic resolution of include paths has been improved for projects with multiple preprocessing configurations.
  • Improved the display of error messages that may be raised during the processing of OIL files for OSEK configuration.

Function locations

The Analysis entry view and the list of function metrics under Overview/Metrics now show the code location (file name, line, and column in the preprocessed code) for each displayed function.

Findings view

The list of message contexts displayed when selecting a finding can now be searched, e.g. to find the contexts with a definite runtime error. Simply press Ctrl+F when the list of message contexts is in focus.

Further changes

  • Improved the upload of original source files to the server to handle analysis projects with a very large number of source files.
  • The value of the option config-file is no longer modified by the DAX export and the corresponding *.cfg file can be downloaded without renaming. The DAX export dialog allows selecting the source files to be downloaded.
  • The built-in preprocessor is now disabled when creating a new project from already preprocessed files using the new project wizard.
  • Fixed the wrapper generator so that it produces correct code even if the user-specified task list has gaps (for example, tasks are specified in line 1 and 3, while line 2 is left empty).

Extensions of the DAX format

  • The commenting mode can be specified in the root element using the attribute comment-mode="AAL" or comment-mode="patterns".
  • The element <annotations> now supports the attribute import.
  • The new comment patterns can be specified in DAX in the following manner: 
    <annotations>
    <comment-pattern classification="..." type="...">
        <comment/>
        <file/>
        <ofile/>
        <oline/>
        <function/>
        <expression/>
        <abstract-expression/>
        <abstraction/>
       <context/>
    </comment-pattern>
</annotations>
    The exact contents of the tags are defined by the analyzer’s internal comment abstraction which can be exported into DAX from the GUI.

Options

  • New options:
    • warn-on-subsequent-uninitialized-reads
      controls whether subsequent reads of uninitialized reads are reported. The option is active by default which corresponds to the behavior of older Astrée releases.
      If the option is disabled, Astrée will raise only one uninitialized read alarm on the following example code, whereas with the default setting two alarms will be reported: 
      void main(void)
{
  int i;
  int a = i;
  a = a & i;
}
    • max-finite-int-set-size=n
      (default 0) controls the domain of finite integer sets which can improve analysis precision on integer values.
    • drop-unused-statics
      controls whether the analyzer omits unused static functions from the coverage information. Enabled by default.
    • widening-with-thresholds
      enables a more precise but also more costly analysis. Disabled by default.
  • The heuristic for the context-insensitive analysis of functions can now be extended by a list of functions that shall not be analyzed in a context-insensitive manner. For example, the option separate-function=*,-f enables the heuristic but ensures that the function f is not analyzed context-insensitively.

Directives

  • __ASTREE_ignore directives no longer need to be preceded by a definition of the respective function. The return value of an ignored function is now considered initialized.
  • The syntax for expressing array slices has been changed from [lo-hi] to [lo..hi]. This affects directives such as __ASTREE_modify. Notifications will be issued when the deprecated syntax is used.

Stub libraries

  • Modified the OSEK stubs to avoid possible name clashes with user-defined resources in OIL files.
  • Modified the OSEK stub library so that task and alarm identifiers can be used in constant expressions. Users that override the TASKNAME macro must now also override the TASK macro.
  • The function pow() in the example C stub library has been generalized to also return negative values.

Server and server controller

  • Clients can now be disconnected via the server controller’s Clients view.
  • The server controller now also displays the license features for analyzers running on a server. This makes it easier to recognize whether a server is configured for Astrée, RuleChecker, or both.

Integration with TargetLink

TargetLink logo
  • Added support for TargetLink 4.2.
  • The Toolbox now supports the new Astrée preference “Use comment patterns”.
  • The latest version of the Toolbox can now be used with older versions of Astrée/RuleChecker, specified under Astree → Preferences.

XML report

The XML result file now includes the analysis project’s <name>, <description>, and <revision> number.

Slicing

The program slicer now supports selecting a specific call context, i.e. a series of function calls leading to the program location of the selected slicing criterion. This new feature is most useful when deriving a sub-program to investigate runtime errors reported in a certain call context.

Wrapper generator

  • Wrapper code generated by the built-in wrapper generator suppresses alarms about missing parameters in function calls. Initialization and periodic functions can be intentionally called without arguments to let the analyzer run with conservative assumptions about the missing parameters.
  • The wrapper generator now introduces additional variable declarations to facilitate project setup.

Improved handling of invalid function calls

  • Astrée no longer stops with an error when a function is called with too few arguments. Instead an alarm is raised, and the analysis continues with the assumption that the missing parameters are initialized.
  • Likewise, the analyzer no longer stops with an error for function calls that provide too many arguments. Instead the runtime error is reported and the analysis continues while ignoring any excess arguments.
  • The analyzer no longer stops in function calls with mismatching types that can’t be resolved by type promotion or a reinterpretation of values. In these cases the analyzer issues an alarm of the form “ALARM (A): invalid function call” and continues with the assumption that affected parameters of the function have arbitrary values.
  • When a function is called via an invalid function pointer, Astrée no longer stops but instead assumes that the function call may be to an unknown function that returns an arbitrary value.
  • In a function call with an incompatible return type that cannot be reinterpreted, the analyzer no longer stops with a definite runtime error. Instead it assumes that the return value is the full range of the expected result type or INVALID if the expected result type is a pointer.

Messages and warnings

  • Enabled suppression and commenting of analyzer alarm messages when running the analysis in parallel mode.
  • The analyzer no longer displays duplicate warnings for overlapping undeclared absolute addresses.
  • Fixed false alarms for correct uses of arrays with only tentative definitions.
  • Fixed a client crash during report generation in batch mode that could be triggered by report configurations that contained a list of analyzer messages grouped by category.

Other changes

  • Shortened the “incompatible types in function call” prefix of some alarms to “invalid function call”.
  • Linking overlapping absolute addresses no longer depends on the order of declarations.
  • Added support for overlapping memory blocks (at absolute addresses) with volatile input specifications. In such cases, the effective volatile range for any part of such memory is the join of all overlapping volatile input specifications.
  • When calling a function with too few arguments while having the option assume-unknown-pointers-are-valid is enabled, Astrée now assumes that these parameters may point to valid memory locations, thus continuing the analysis even when they are dereferenced.
  • It is now possible to read absolute addresses encoded in char arrays to initialize pointers. Example: 
    unsigned char mem[] =
  { 0, 0, 0, 0x2A, 0, 0, 0x10, 0x0C,
    0, 0, 0, 0x17, 0, 0, 0x05, 0x39, };
__ASTREE_absolute_address((mem, 0x1000));
  
typedef struct A { int  a; int* b; int  c; } A;
  
int main(void) {
  A* p = (A*)0x1000;
  /* now Astree knows precise values for all members of 'p'
     including that p->b points to 0x100C */
}
  • Partial initializers for variables of type struct with flexible array member are now supported.
  • The analyzer now supports the interpretation of pointers as enum values. Code like the following can now be analyzed: 
    enum E { A } e = (int*)0;
  • When raising an invalid dereference due to offset overflow, e.g. by using a potentially-too-large value as array index, Astrée now removes all incorrect offsets, rather than a select few. This prevents undesired subsequent alarms following an invalid dereference due to incorrect offsets.
  • When generating absolute addresses, Astrée now limits what addresses are valid based on the size of pointers declared in the ABI.
  • Astrée now fully supports GCC extended assembler statements, i.e. it soundly approximates all reads and writes on program variables, as specified by the extended assembler syntax.

Bug fixes

  • Fixed the file filter for rule violations configured in Overview → Findings or the custom report configuration. It previously had no effect on the lists of findings displayed in the Findings view or the custom report files, respectively.
  • Fixed an analyzer crash when using variables with overlapping absolute addresses containing volatile parts while having the option volatile-global or volatile-static enabled.
  • Fixed exceptional aborts of the analyzer that could occur when enabling the option separate-with-caller-stack-pointers.
  • Fixed an exceptional abort of the analyzer that could occur when analyzing asynchronous programs.
  • Fixed an issue that could cause the analysis to not terminate when enabling the octagon domain on code with recursive function calls.
  • Fixed cases of missing or incomplete invariants collected with the option export-invariant and displayed in the watch window.
  • Fixed an issue that could cause the analyzer to stop with the error message “Failure(‘Wrong type for a struct’)”.
  • Fixed an issue that could cause modified analysis settings to get lost when hitting the analysis start button.

RuleChecker

See the dedicated release notes for RuleChecker 17.10.