Astrée release 18.04

Support for C11

  • The C frontend now fully supports the ISO/IEC 9899:2011 language syntax.
  • The C stub library is now compliant with C11, with new new header files, macros, types, and functions.

Floating licenses

Astrée and RuleChecker now support floating licenses in addition to node-locked licenses. Any existing node-locked license can be upgraded to floating if desired. Contact support@absint.com with any questions.

CompCert support

Astrée now includes target-specific configurations for CompCert, ensuring that the analyzer considers the correct ABI for each target and soundly approximates CompCert’s built-in functions.

Integration with TargetLink

  • The AbsInt Toolbox for TargetLink now automatically enables the Gauge domain.
  • The Toolbox now generates additional __ASTREE_suppress directives when specifying ranges for const volatile declared calibration parameters in order to avoid justified but undesired alarms about writes to constant memory.
  • If a DAX file specifies a wrapper-and-stubs file as well as a TargetLink data dictionary, the configuration generated from the data dictionary no longer overwrites the wrapper-and-stubs-file, but is appended to it.
  • The Interpolation domain now computes more precise invariants for interpolation functions generated by TargetLink.

Qualification Support Kits

  • Seven new test cases for Astrée.
  • 28 new test cases for RuleChecker.
  • Five test cases are now obsolete and have been removed (qk_check_mline_comment, qk_check_other_escape_sequence, qk_check_static_declaration, qk_alarm_initializer_range, qk_option_dependencies).

Windows support

The Astrée client now handles longer paths on Windows, up to 247 characters.

Full support for C11

The C frontend now fully supports the ISO/IEC 9899:2011 language syntax, including:

  • generic selection
  • anonymous structures and unions
  • _Noreturn functions
  • _Alignas specifiers
  • _Alignof operator

Other improvements

  • The C frontend now also supports:
    • 64-bit bitfields
    • statement expressions that contain declarations of static variables
    • lvalue casts at the left-hand side of assignments
  • The frontend now checks for, and rejects:
    • struct or union types having members of incomplete type (except for flexible array members)
    • lvalue expressions of incomplete type, which is undefined behavior
  • Forward-declared enumerations are now treated as incomplete as long as no enumerator-list has been given. The new behavior is consistent with that of GCC.
  • When calling implicitly declared functions, the C frontend now uses the visible type declaration, even if the concrete type of the callee is already known from a previous translation unit.

Original-source frontend

  • The frontend now can handle an empty macro argument as operand of the # operator.
  • Improved the evaluation of the # operator in the frontend’s internal preprocessor to omit superfluous whitespace in the resulting string-literal.
  • Fixed an exception in the original-source parser which occurred when parsing a preprocessing number which is not a valid number constant (e.g. 0xx0).

Client

  • The temporary directory of the client is now displayed in the Information view.
  • The preprocessor output view now provides a horizontal scroll bar for very long lines of output.
  • The tables in Overview → Reachability and Overview → Not Reached now allow adding functions to the wrapper generator via the context menu.
  • The mechanism for inserting annotations into the code via the GUI has been improved and is more robust now.
  • The call graph is no longer loaded automatically when opening an analysis project. Instead you must explicitly request the graph to be loaded in the Call graph view. This lets you open analysis projects with extremely large call graphs that might otherwise cause the GUI to run out of memory.
  • The profiling information accessible via Tools → Analysis Time has been improved to produce more accurate timing statistics when using the option separate-functions or analyzing asynchronous code.

Server controller

  • The server controller’s Clients tab now also shows the names of connected users.

Bug fixes

  • Fixed occasional crashes when using the Filter feature in the Overview.
  • Fixed an issue that could cause the client to crash when using the global version of the __ASTREE_comment directive in an AAL annotation.
  • Fixed an issue that could cause the server to hang when several analyses to be run in parallel were started in rapid succession.

Compiler configurations

The share directory of the installation now contains target-specific configurations for CompCert. Loading such a configuration ensures that the analyzer considers the correct ABI for that target and that it understands and soundly approximates all built-in functions of CompCert for that particular target.

Extensions of the DAX format

  • DAX files may now contain more than one <external-declarations/> section. The declarations from subsequent <external-declaration/> sections are appended to already imported declarations. Moreover, <external-declaration/> sections can now be imported from other DAX files.
  • DAX files can now refer to shared files in the installation directory of Astrée/RuleChecker by using the $A3_SHARE_DIR variable. It can be used for importing ABI and compiler configurations that are shipped with the tool. For example:
    <abi import="${A3_SHARE_DIR}/abi/ppc32.dax">
  • DAX files can now import the <preprocess/> section from other DAX files. The imported configuration can be extended by further preprocessing configurations.

ABI

  • The following types can now be configured:
    • size_t
    • ptrdiff_t
    • wchar_t
    • wint_t
    • char16_t
    • char32_t
    • intptr_t
    • intmax_t
    • sig_atomic_t
  • New option max_atomic_width for specifying the maximum width lock-free atomic operation supported by the target.

New options

  • clamp-out-of-bound-array-index
    cuts execution traces that lead to array-index-out-of-bounds alarms. The severity of array-index-out-of-bound alarms changes from C to A. After such an alarm the analysis continues with only the valid indices. This avoids successive array index out-of-bound alarm on the same variable for the same bounds. This option is enabled by default.
  • warn-on-stub-invocation
    controls whether or not the analyzer raises alarms when calling automatically generated stub function. The alarms are enabled by default.

New batch mode options

  • --export-preprocessed <target-directory>
    exports the preprocessed files into the specified directory
  • --export-aal <filename>
    writes the AAL annotations of an analysis project to the specified file with no user interaction
  • --export-entry-functions <file.xml>
    exports the list of functions collected by the analyzer if the option list-entry-functions is enabled
  • --export-only
    for use with the options --export or --export-aal, to prevent the analysis from being executed and only perform the specified export actions

Directives

  • New directive __ASTREE_check_separate_targets, which takes as argument a list of (at least two) lvalues, and checks if any two of them may point to the same variable. If that is the case, a “Check failure” alarm is emitted, including the actual bytes pointed to in the variable.
  • The directive __ASTREE_volatile_input now uses the syntax lo..hi for index ranges:
    __ASTREE_volatile_input((a, { 0..2: [23, 42] }));
    The old syntax lo-hi is now deprecated.
  • Invalid integer ranges such as [1..0] in directives are now reported as errors in addition to ignoring the erroneous directive.
  • Removed duplicate error messages for incorrect expressions used in directives.
  • Erroneous directives that have been skipped by the frontend no longer appear in the /* Semantic hypotheses */ section of the analyzer output.
  • Fixed the placement of directives via AAL when addressing labels with insert before. In previous versions the directive was incorrectly placed after the label rather than in front of it.

Preprocessor settings

  • You can now specify a programming language (C/C++) for each preprocessor configuration.
  • The preprocessor now runs with the C version configured under Options → General → C Language Version. The default version is C99.
  • The new option --cxx-version controls the version of C++ that is assumed when preprocessing and checking C++ code. The default version is C++14.
  • The internal preprocessing now always runs in a fresh directory within the client’s temporary directory. The following preprocessor settings are therefore obsolete and have been removed:
    • Destination directory
    • OSEK output directory
    • Empty destination directory before preprocessing
    • Use paths relative to destination directory for preprocessed files (paths are now always relative)
  • Likewise, the following DAX settings no longer have an effect:
    • <preprocessor>’s child element <destination> together with its attribute delete-files
    • <preprocessor>’s attribute use-relative-paths
    • <osek>’s child element <output-directory>

Alarms

  • Astrée now cuts traces leading to divisions by 0 when the option cut-integer-division-by-zero is set, so that consecutive alarms do not occur.
  • Astrée now emits a class A alarm when detecting writes to constant memory. The analysis then carries on with the assumption that the write succeeded.
    Note that alarms about writes to constants are also raised when using __ASTREE_modify for specifying ranges for calibration parameters declared const volatile. The wrapper generator and the latest version of the AbsInt Toolbox for TargetLink both suppress these warnings by generating additional __ASTREE_suppress directives.
  • If the option warn-read-of-never-written-variables is set, Astrée now also raises an alarm when a global variable is read that was only initially set to 0 but not explicitly written to.
  • The analyzer no longer issues alarms of the form
    <type> initializer range <value> not included in [interval]
    Instead, it raises an alarm of the form
    <type1> -> <type2> conversion range [interval] not included in [interval]

Messages and warnings

  • The option dump-data-dictionary now prints static variables in the same format that is accepted when specifying input ranges for static variables in the wrapper file. Example:
    data-dictionary:
       static_var_name@"file_name.c" of type signed int in {1} / != 0
  • Improved error messages during constant propagation (only used if the option simplify is enabled).
  • When calling the __astree_exit() intrinsic, Astrée now prints a notification message instead of a mere plain text message.

Report files

  • Alarm comments and classifications from the source directive ASTREE_comment are now also included in HTML report files.
  • Improved layout of long lines in HTML reports.
  • Automatically stubbed functions are now listed in the <functions/> section of the XML report file.
  • The XML report file now includes the analysis type, using the new attribute type of the <analysis/> tag. The possible values are Astree and RuleChecker.
  • The Output view and text report files now contain more detailed version and configuration information for the built-in preprocessor.
  • In both the Output view and text report, the analysis summary is now printed at the very end of the log, after postprocessing and printing of memory statistics.

Miscellaneous

  • Floating point numbers are now rounded upwards for printing in all circumstances. In previous releases, on machines with glibc version <2.17, floats were sometimes rounded to nearest. Note that this only affects printing, e.g. when logging invariants of the analyzer’s abstract domains.
  • If the option dump-dataflow is disabled, the analyzer no longer writes unused data flow information to the result files.
  • Not reached AAL annotations are now included in the list of not reached code locations.

Bug fixes

  • Fixed the classification of directives as semantic hypotheses and further directives in the analyzer text output. This affects the directives __ASTREE_known_range, __ASTREE_trash and __ASTREE_check_separate_targets.
  • Fixed printing of the directive __ASTREE_smash_variables.

RuleChecker

See the dedicated release notes for RuleChecker 18.04.

Stub libraries

  • Improved the C stub library to make it compliant with C11, in particular adding new header files, macros, types, and functions required by C11.
  • The C stub library is now preprocessed without errors and warnings if the ABI defines attributed pointers, or sets long long or long double to only 4 bytes.
  • Modified the setjmp() and longjmp() stubs library to make them syntactically valid in all circumstances.
  • The fgets function has been modified to allow for more precise analysis results when reading up to 1024 bytes.
  • The setlocale function now handles NULL pointer arguments.
  • The lconv struct returned by the localeconv function is now always initialized.
  • The implementation of the signal function now handles more possible behaviors.

Preprocessor

  • The built-in preprocessor now converts trigraphs.
  • The preprocessor can now process files on ClearCase MVFS drives.

Slicing

  • The program slicer output now contains information about the maximum amount of memory that has been used during a slicer run.
  • Function parameters not used in a slice are now marked with the comment /* removed parameter */.

Wrapper generator

  • Input specifications for arrays and structs are now supported.
  • Specifying the type of inputs in the wrapper generator is no longer required.
  • Variable declarations for input variables are no longer generated.
  • Additional __ASTREE_suppress directives are now generated when specifying ranges for inputs, to avoid justified but undesired alarms about writes to const volatile declared variables (e.g. calibration parameters).

Other changes

  • Improved the interpolation domain to increase precision of computed invariants for interpolation functions as e.g. generated by the dSPACE TargetLink code generator.
  • Improved the determination of function calls in the separate function heuristics, so that more candidate functions for a context-insensitive analysis are now considered when the option separate-function=* is set.
  • The analyzer no longer attempts to export an AIS file if the runtime analysis was skipped because of the option skip-analysis=yes.
  • The analyzer option dependencies has been removed. Whether the analyzer uses the abstract domain of arithmetic-geometric progression now only depends on the option dev-geo.
  • Static variables can now be referenced in the wrapper-and-stubs file by using the syntax extension variablename@"filename". Here are three examples for specifying the initial ranges of such variables:
    __ASTREE_modify((x1@"file1.c"; [1,1]));
    __ASTREE_modify((x2@"file2.c".field1; [42,42]));
    __ASTREE_modify((x3@"file3.c"[2]; [17,17]));
    
  • Erroneous directives that are discarded by the frontend are now marked as unreachable.
  • Functions that have been excluded from the analysis by means of the directive __ASTREE_ignore are no longer marked green in the editor view.

Bug fixes

  • Fixed exceptional aborts of the analyzer that could occur:
    • when using dynamic smashing in conjunction with the analyzer-intrinsic function __astree_bzero
    • when enabling both the octagon domain and the interpolation domain
    • in rare cases when using the option dynamic-smash-variables-threshold
    • when encountering a recursive function call that returns a function pointer
    • when combining the options dynamic-smash-variables-threshold, generate-undeclared-absolute-addresses, and assume-unkonwn-pointers-are-valid
  • Corrected a display issue that in some situations could lead to missing green markers for proven code.