Astrée and RuleChecker release 18.04

RuleChecker for C++

RuleChecker can now analyze C++ code. This release introduces support for a majority of MISRA C++:2008 rules.

Floating licenses

For both Astrée and RuleChecker, floating licenses are now available 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.

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.

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.

Support for macOS

On request and for an additional fee, RuleChecker is now also available for macOS High Sierra 10.13 or newer.

Portable version

For all operating systems, the portable version now comes as a ZIP file. The top-level directory within is named like the file itself, including the build number, with the .app suffix added on macOS. This prevents different builds from overwriting each another upon unzip.

Under Linux, the ZIP file also contains the install script, should you later decide to install the software rather than running it from the unzipped directory.

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

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 ABI now allows to configure the following types:

    • size_t
    • ptrdiff_t
    • wchar_t
    • wint_t
    • char16_t
    • char32_t
    • intptr_t
    • intmax_t
    • sig_atomic_t
  • New ABI option max_atomic_width for specifying the maximum width of 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>

Other

  • Paths in RuleChecker configurations containing “..” are now normalized in batch mode execution as well. This does away with error messages of the form
    Unknown file in RuleChecker configuration: /a/path/with/../in/it.c
  • The configuration-specific base directory is now also applied to automatic includes.

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.

Improved reporting

  • 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.
  • Rule violations detected during runtime error analysis are now printed with full context information.
  • The analyzer no longer emits type C alarms about statically evaluable expressions when no runtime error analysis is performed.

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.
  • The Windows version can now handle longer paths, up to 247 characters.

Server controller

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

Other changes

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

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).
  • 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, as e.g. generated by TargetLink.

Other changes

  • 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.
  • Type abbreviations for array types are now supported.
  • Syntactically invalid conditions in an inactive #if directive no longer trigger error messages.
  • Rule checks are now also applied to size expressions of array declarators and to case labels.
  • Parser filters are no longer applied to #include directives when rule checking.
  • The check struct-type-incomplete now also reports non-compliant anonymous struct types, and no longer issues alarms for opaque pointers to structs/unions: 
    struct ST *p; // Compliant even if no definition for ST is given

Qualification Support Kits

  • Parallel execution of test cases is now supported, customizable via the new option “Number of concurrent test cases”. The default is 1, and the special value “auto” parallelizes the execution across all CPU cores.
  • The naming pattern for accepted QSK packages in the Qualification dialog has been fixed.
  • 19 new test cases for Astrée:
    • qk_abi_size_t
    • qk_abi_ptrdiff_t
    • qk_abi_wchar_t
    • qk_abi_wint_t
    • qk_abi_char16_t, qk_abi_char32_t
    • qk_abi_intptr_t, qk_abi_intmax_t
    • qk_abi_sig_atomic_t
    • qk_option_cxx_version
    • qk_option_warn_on_stub_invocation
    • qk_option_clamp_out_of_bound_array_index
    • qk_option_config_file
    • qk_option_merge_separate_contexts
    • qk_directive_check_separate_targets
    • qk_commandline_export, qk_commandline_export_aal, qk_commandline_export_preprocessed, qk_commandline_export_only
  • 34 new test cases for RuleChecker:
    • qk_rule_a_1_7, qk_rule_a_1_9, qk_rule_a_1_8, qk_rule_a_2_10, qk_rule_a_5_2
    • qk_rule_cwe_476, qk_rule_cwe_561
    • qk_rule_s_typ_2_1, qk_rule_s_typ_2_2, qk_rule_s_typ_2_3
    • qk_abi_max_atomic_width
    • qk_check_union_typedef_name, qk_check_union_typedef_name_max_length, qk_check_union_typedef_name_min_length
    • qk_check_assignment_to_non_modifiable_lvalue
    • qk_check_redeclaration
    • qk_check_initializer_excess
    • qk_check_excessive_interval
    • qk_check_invalid_directive
    • qk_check_min_comment_density_his
    • qk_check_binary_constant
    • qk_check_hexadecimal_escape_sequence
    • qk_check_include_characters_backslash
    • qk_check_unsupported_language_feature
    • qk_check_mmline_comment, qk_check_smline_comment
    • qk_check_static_function_declaration, qk_check_static_object_declaration
    • qk_check_universal_character_name
    • qk_commandline_export, qk_commandline_export_preprocessed
    • qk_directive_comment_source
    • qk_option_cxx_version
    • qk_option_type_abbreviations
  • 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).

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.
  • Fixed false alarms for the check function-pointer-integer-cast when analyzing expressions involving null pointer constants.
  • Fixed an issue that could cause macro definitions for specific configurations to be applied to all files during rule checking.
  • Fixed missing RuleChecker alarms about potential side effects for calls to functions without definition when using the option auto-generate-stubs=no.

MISRA C++:2008

This is the first stable release of RuleChecker to support checking C++ code for compliance with MISRA C++:2008 rules.

MISRA-C:2004 and MISRA-C:2012

  • Improved precision of the side-effect analysis in the presence of array look-ups. This removes false alarms for the checks multiple-volatile-accesses and logop-side-effect, and the respective rules M.12.2, M2012.13.2, and M.12.4.

  • The default parameter of rule M.3.4 has changed such that it now rejects all uses of #pragma.
  • The rule arguments for M.19.2 and M2012.20.2 have been removed, as the distinction they supplied is no longer necessary. The relevant check include-characters has been split into the two checks include-characters and include-characters-backslash.
  • The check for rule M.5.1 is now also applied to macros.
  • Violations of the check non-standard-keyword are now also reported for the keywords typeof, __asm, __asm__, and __alignof__. This affects rule M2012.1.2 and M.1.1.
  • The checks statement-sideeffect and expression-statement-dead now warn about statements containing the ?: operator if at least one branch has no side effect. This affects rule M.14.2 and M2012.2.2.
  • Removed false alarms for rule M.19.5 by restricting the check define-in-block to function bodies.
  • The check type-compatibility (rule M.8.4) now uses the unqualified types of function parameters when checking for type compatibility.
  • In rare circumstances, RuleChecker considered a call to a function without definition a persistent side effect with respect to rule M2012.13.5. This has been fixed.
  • The check identifier-hidden now warns about hidden tags. This affects rule M.5.2.
  • The following checks have been extended to preprocessing directives:
    • octal-constant (M.7.1, M2012.7.1)
    • octal-escape-sequence (M.7.1)
    • other-escape-sequence (M.4.1)
  • The checks for M.12.11 and M2012.12.4 now also cover integer constant expressions where permitted by the standard (e.g. in switch cases, array designators, and enumeration constants).
  • The check bitop-type now also checks the sign of the right-hand side of shift operators (<<, >>, <<=, >>=). Furthermore, it now considers signed integer constants of positive value as underlying signed and reports rule violations in such cases. This affects rule M.12.7.
  • Removed false alarms for M.1.1, M.11.5, M2012.1.1, and M2012.11.8 when casting or assigning a string literal to a pointer to non-const char.
  • RuleChecker now warns about violation of rule M.1.1, M.11.5, M2012.1.1, and M2012.11.8 when accessing a struct or union member where the base object is qualified but the accessed member is not. Example: 
    const struct { int non_const_qualified_member; } const_qualified_structure;

// assignment-to-non-modifiable-lvalue
const_qualified_structure.non_const_qualified_member = 0;

// pointer-qualifier-cast
(int *) &const_qualified_structure.non_const_qualified_member;
  • The check identifier-unique-typedef (rule M.5.3, M.5.6, M.5.7, and M2012.5.6) now reports the locations of both the typedef and the conflicting occurrence.
  • Fixed false alarm for check identifier-unique-tag in case of forward-declared structs. This affects rule M.5.4, M.5.6, M.5.7, and M2012.5.7.
  • Fixed the handling of type qualifiers for arrays. This affects the checks type-compatibility (rule M.8.4) and parameter-missing-const (rule M.16.7, M2012.8.13).
  • The check reserved-identifier now warns about any identifier starting with an underscore, including identifiers of the standard library. This affects rule M.20.1, M2008.17.0.1, and M2012.21.1.
  • The check integral-type-name in rule M.6.3 and M2012.D.4.6 no longer warns about the use of _Bool, _Complex, and _Imaginary. The only check to warn about these type names is now integral-type-name-extended in rule X.A.5.6.

MITRE CWE

  • Added support for rule CWE.476 and rule CWE.561.
  • Extended support for CWE.125, CWE.126, CWE.127, CWE.190, CWE.191, and CWE.823.

SEI CERT Secure C

  • Improved precision of the side-effect analysis in the presence of array look-ups. This removes false alarms for the checks multiple-volatile-accesses and logop-side-effect, and the respective rules CERT.EXP.2, CERT.EXP.10, and CERT.EXP.30.
  • The checks statement-sideeffect and expression-statement-dead now warn about statements containing the ?: operator if at least one branch has no side effect. This affects rule CERT.MSC.12.
  • The check reserved-identifier now warns about any identifier starting with an underscore, including identifiers of the standard library. This affects rule CERT.DCL.37.
  • The check bitop-type now considers signed integer constants of positive value as underlying signed and reports rule violations in such cases. This affects rule CERT.INT.13.
  • The check type-compatibility for rule CERT.DCL.40 now uses the unqualified types of function parameters when checking for type compatibility.
  • The check octal-constant for rule CERT.DCL.18 has been extended to preprocessing directives.

ISO/IEC TS 17961:2013

The check reserved-identifier now warns about any identifier starting with an underscore, including identifiers of the standard library. This affects rule ISO.17961.44.

Diagnostics

  • New rules:
    • A.1.7 warns about modifications of non-modifiable l-values.
    • A.1.8 together with the check initializer-excess warns about braced initializer lists exceeding the size of the object initialized.
    • A.1.9 together with the check redeclaration warns about re-declarations of an identifier without linkage in the same scope.
    • A.2.10 warns about binary constants such as 0b0101 (GCC extension).
    • A.5.1 warns when an invalid directive is dropped or when a directive contains an interval that exceeds the range of values of the respective type.
  • Violations of the check non-standard-keyword are now also reported for the keywords typeof, __asm, __asm__, and __alignof__. This affects rule A.2.7.
  • Fixed the handling of type qualifiers for arrays. This affects the check type-compatibility (rule A.1.1).
  • RuleChecker now warns about violation of rule A.1.7 when accessing a struct or union member where the base object is qualified but the accessed member is not. Example:

    const struct { int non_const_qualified_member; } const_qualified_structure;

// assignment-to-non-modifiable-lvalue
const_qualified_structure.non_const_qualified_member = 0;

// pointer-qualifier-cast
(int *) &const_qualified_structure.non_const_qualified_member;
  • The check type-compatibility (rule A.1.1) now uses the unqualified types of function parameters when checking for type compatibility.

Style and naming rules

  • New naming rules S.TYP.2.1-3 for checking the naming of typedefs for union types.
  • The S.1.x naming rules have been replaced. Old analysis configurations that enable these rules are automatically converted as follows:
    • S.1.1 → S.MCR.0.1
    • S.1.2 → S.OBJ.0.1
    • S.1.3 → S.TYP.0.1
    • S.1.4 → S.FCT.0.1
    • S.1.5 → S.ENM.0.1

Customer-specific rules

  • Added exceptions for rule X.B.5.1: the constants 0 and 1, and enumeration constant definitions.
  • Rule X.B.5.4 has been changed to use the check precedence, which checks that expressions are parenthesized according to MISRA-C:2012 rule 12.1.
  • Fixed false alarm for rule X.B.3.5 (check identifier-unique-tag) in case of forward-declared structs.
  • The check identifier-unique-typedef (rule X.B.3.5) now reports the locations of both the typedef and the conflicting occurrence.
  • The check identifier-hidden now warns about hidden tags. This affects rule X.A.5.14.
  • The checks octal-constant, octal-escape-sequence, simple-escape-sequence, and other-escape-sequence for rule X.A.3.8 have been extended to preprocessing directives.