Astrée and RuleChecker release 19.10

Streamlined messages

The concept of “Notification” messages has been removed from the tool:

• Messages with mere informational character (e.g. usage hints) now appear only in the analyzer log and in the text report file.
• Notifications about issues with the analyzer configuration have been mapped to diagnostic rule checks.
• A few select notifications are now instead reported as alarms of the new class D.

Higher precision

• The analyzer is now more precise when computing pointer differences in integer types, and generally more precise when computing pointer differences for C++ code.
• The analysis model for asynchronous code now supports sequential phases of execution. Each task can be assigned to one or several sequential phases. Tasks in the same phase are executed concurrently and can rely on tasks in earlier phases to have already been executed. This new feature allows for a more precise analysis, in particular of code with initialization tasks that need to run before all other tasks.
• Improved the precision of the analysis by taking into account bit-field information for intervals.
• Improved precision when analyzing struct copy operations, e.g. when assigning to whole structs or passing them as parameters in function calls.
• Improved the precision on bitwise operations.
• Improved the auto-unroll feature to consider more loops for automatic unrolling.
• __ASTREE_assert and __ASTREE_global_assert directives no longer prevent the domain of arithmetic-geometric progressions (controlled by the option dev-geo) from computing precise bounds.
• Improved the precision of the analysis in the presence of global assert directives.
• Improved the effect of __ASTREE_modify with a value range argument (such as [1, 9]), so that it performs a strong update when given as first argument a generic array access with structure access (such as t[].a). The previous behavior (weak update) was sound but imprecise with regard to the documented semantics.

Improved performance

• Improved the performance of initialization tracking. Analysis projects that formerly required initialization tracking to be disabled can now re-enable initialization tracking, i.e. remove the support option warn-on-uninitialized=no.
• Improved the efficiency of function calls in partitioned contexts.

New Astrée features

• Added a new automatic partitioning heuristic for partitioning sequences of switch statements over the same variable. The heuristic can be deactivated by disabling the new option partition-multiple-switches.
• The astree-cxx analysis mode for run-time error analysis of C++ code now also supports C++ rule checks. Both run-time error analysis and rule checking can thus be executed in a single analysis run.
• New option partition-predicate-functions that permits partitioning of function calls in conditions. This allows for a more precise analysis of code like

  if (predicate(x)) { ...  }

  The new option is disabled by default. The value * enables heuristic partitioning. It is also possible to explicitly add or remove functions from the partitioning.
• Improved file handling in the presence of symbolic links to resolve issues with not found files during rule checking.
• Added analyzer-intrinsic __astree_not_a_number() that evaluates to NaN and is considered a constant expression.
• Added a new option for controlling the output of result tables in the text report file and analyzer output view. By default, the tool now only reports the table of reached functions (with coverage) and the number of findings per alarm category. Further tables, e.g. not reached functions, stubbed functions, or the list of findings per file, can be enabled by the new option text-report-tables.

Improved metrics

• Higher precision of the metric PATH, by no longer ignoring deeper nested case/default labels as well as break, continue and return statements.
• The LSCOPE and SoS metrics now also take the typeof operator into account.
• For C code, the LSCOPE and SoS metrics now consider the keyword else, and take into account case and default labels.
• The metric LOCVAR now also considers local function declarations, typedefs, extern declarations, and member declarations, if any of these constructs appear inside of function bodies.
• Fixed computation of the metric LEVEL for code in which the maximum depth is encountered in the first then-branch of an else-if.
• asm statements are now considered when computing metrics.
• Improved calculation of the C code metric PATH:
  • It now yields more precise results for switch cases that are only left by break or return.
  • Updated the formula for computing the metric on for loops.
  • Control flow in extended asm statements is now also considered.
• The CDFILE metric now considers all characters in comments ending in a **/

• All the following code metrics are now also available for C++ code:

  • CALLS (# of called functions)
  • CALLING (# of functions calling a function)
  • CDFILE (comment density of a file)
  • CYCL (cyclomatic complexity)
  • FILES (# of original source files)
  • FUN (# of function definitions)
  • GOTO (# of goto statements)
  • LEVEL (nesting depth of control structures)
  • LINE (# of source lines)
  • LOCVAR (# of local variables)
  • LSCOPE (Language Scope)
  • MLINE (# of maintainable code lines)
  • PARAM (# of parameters)
  • PATH (# of execution paths)
  • PLINE (# of physical source lines)
  • RETURN (# of return statements)
  • RPATH (# of recursive paths)
  • STMT (# of instructions)
  • SoS (size of statement)

Frontends and preprocessor

• Now using version 9 of LLVM/clang.
• Warning messages issued by the Clang frontend are now reported as violations of the new diagnostic rule A.6.2 (clang-warning).
• The keyword asm is now accepted and ignored as a declaration specifier by the C frontend.
• Added support for GCC’s built-in function __builtin_constant_p.
• The C frontend now supports enumerators that exceed the range of signed int.
• The C frontend now directly supports CompCert’s built-in function __builtin_sel.
• Fixed erroneous rejection of valid AAL annotations due to supposed file name ambiguity.
• Suppress directives now take precedence over comment directives. That is, commented alarm messages can now be suppressed.
• The C frontend now supports:
  • the attribute 'packed' when used with struct (member) declarations in the following forms
    • __attribute((packed))
    • __attribute((packed(1)))
    • __attribute((packed(1, 2)))
    • __attribute__((packed))
    • __attribute__((packed(1)))
    • __attribute__((packed(1, 2)))
  • the __packed__ type specifier, which is handled analogously to the packed attribute
  • the attribute aligned in the following forms:
    • __attribute((aligned))
    • __attribute((aligned()))
    • __attribute((aligned(1)))
    • __attribute__((aligned))
    • __attribute__((aligned()))
    • __attribute__((aligned(1)))
  • _Alignas() in type declarations, e.g.

    typedef _Alignas(8) int aligned_int;

  The effects of these attributes and specifiers are also semantically taken into account by the analyzers whenever appropriate.

DAX

• Added new tags <paths/> and <path/> for including/excluding files and folders into/from rule checking (see also release notes for RuleChecker).
• Renamed two attributes so that their meaning corresponds to the wording used in the tool.
• For the <include-alarms> tag, the attribute type has been renamed into class.
• For the <comment-pattern> tag, the attribute type has been renamed into category.

<!-- DAX file excerpt showing the modified attributes -->

<reports>
  <report-configuration>
    <results>
      <findings>
        <include-alarms class="...">
 
  <annotations>
    <comment-pattern classification="..." category="...">

Alarms, messages and warnings

• The concept of “Notification” messages has been removed from the tool. Messages with mere informational character (e.g. usage hints) now appear only in the analyzer log and in the text report file. Messages about issues with the analyzer configuration have been mapped to diagnostic rule checks.
• Introducing new alarms of class D (data and control flow) to replace former notification messages:
  • The alarm control_flow_anomaly has the form

    ALARM (D): Function call to ... never returns in this context

    or

    ALARM (D): Analyzed entry-point ... never returns

    It is controlled by the option warn-on-control-flow-anomaly and enabled by default.
  • The alarm loop_unbounded has the form

    ALARM (D): Loop may be unbounded

    It is controlled by the options warn-on-unbounded-loop and gauges (both must be active) and disabled by default.
• Removed false alarms about non-terminating loops for loops that can only be left via return statements.

• The GUI now asks for confirmation when deleting critical data, e.g. analysis revisions or annotations.

Improved reporting

• Report files that have not been generated yet are marked by a red icon in the GUI.
• The text report file is now generated even if generating other report files fails.
• The analyzer now displays for each alarm message an excerpt of the code that is affected by the run-time error or rule violation. The maximum number of extracted code lines can be controlled by the new option code-lines (default is 3). Code excerpts are displayed in the GUI and are contained in the text and XML report files. Example:

  [ call#main at astree.cfg:18.0-50.1
  call#basic_examples at astree.cfg:26.6-22
  loop=11/12 at scenarios.c:72.6-73.26
  ALARM (A): out-of-bound array index {10} 
  not included in [0, 9] at scenarios.c:73.19-20 ]
  > ArrayBlock[i] = i;
  >            ~

• In all reports, error messages are now consistently prefixed with ERROR:.

Improved tooltips

• The GUI now displays more detailed tooltip information when:
  • an integer variable contains the address of an object,
  • a function pointer is used in the context of data pointer.
• Tooltips now also display modulo, bit, and non-zero information computed by the analyzer.

Server and server controller

• Analysis servers now support personalized administrator accounts with configurable roles for technical and user administration. Accounts and roles are configured in the server controller user management.
• The server controller now provides a batch mode interface. It covers all features that are available in the controller GUI, e.g. starting and stopping the server, displaying information, and modifying server settings.
• Remote servers that are added to the server controller by explicit specification of their IP addresses are now also displayed with their host names instead of their IP addresses.
• The process of registering the a³ for C Server of an existing installation as a Windows service has been fixed and moved into the server controller.
• The server controller GUI now permits deleting a linear history leading up to a selected revision of a project.
• Improved the server log file. It now contains more information about administrative actions and analysis runs. The new message format is also better structured, to simplify automatic processing of the server log file.
• Fixed an issue that could lead to a non-terminating action on the server, effectively blocking a client connection. The issue could be triggered by a client attempting to export project data into an AAF file.

Client GUI and batch mode

• The client GUI now permits deleting a linear history leading up to a selected revision of a project.
• Improved client/server performance when re-running an analysis project with original source files that have not been modified since the last analysis run.
• The project ID can now be exported to DAX. The DAX export dialog provides a corresponding option (disabled by default).
• Fixed an issue that caused C++ RuleChecker alarm comments to get locked, so that they could not be modified by the user in the Findings view.
• Unused comments for C++ rule violations are now added to the list of "Unused Comments" in the Findings view.
• Missing directories of report file path settings are no longer created automatically. If the path does not exist, the report file is either not generated (GUI execution), or the tool aborts with an error message (batch mode execution).
• The columns in the control flow table of the results overview can now be sorted.
• The search results of the identifier and full text searches can now be exported to .csv.
• Corrected the import of version 1.4 DAX files that contain a custom report configuration of the form

  <report configuration>...
    <results>...
      <findings>...

• Fixed a performance and stability issue when using the search features in the Overview tabs of the client in release 19.04.
• Changed the behavior when a project ID and/or base revision is specified both in DAX file and on the command line via --id or --revision. The option specified on the command line now consistently takes precedence over the value from the DAX file.
• Added new batch mode options --analysis-name and --analysis-description for specifying the analysis name and description on the command line. The command line options take precedence over the values specified in DAX.
• The Information View has a new field “Batch command line” that displays the command line used to run the analysis in batch mode (-b or -B). The value is empty for analyses that are started manually from the client. If the analysis has been run multiple times, the value of the latest analysis run is displayed. The batch command line is now also available in all report files (text, XML, and custom).
• The GUI no longer opens dialog windows for displaying progress of long-running actions. Instead it displays a progress bar in the lower right corner of the main window.
• AAL Annotations with parse errors or insertion errors are now marked with a red icon in the Annotations view.
• Enabled modifying the RuleChecker option type-abbreviations in the GUI.
• Fixed an issue that could lead to missing file names in report files.
• Overview → Metrics now supports filtering, using Ctrl+F.
• Custom reports can now be configured to refer to analyzed files with absolute paths. This feature can be enabled via the custom report configuration Results → Absolute file names) or in DAX:

  <reports>
    <report-configuration>
        <results absolute-file-paths="yes">

• The table “Findings by category” in the text report file and in the Output view of the GUI now also take alarms into account that the analyzer reports during the evaluation of constant expressions. This fixes inconsistencies between this table and the Findings/C overview in the GUI.
• Improved editor highlighting and tooltips for source code expressions that are affected by simplification, when setting the option simplify=yes.
• The import of preprocessor configurations via the DAX tag <preprocess import="..."/> now also takes the global <base/> tag of the imported <preprocess/> sections into account.
• RuleChecker findings for whole files, without line or column information (e.g. “check min-comment-density failed”), can now be commented on in the GUI.
• Fixed an issue that in release 19.04 and 19.04i could lead to incorrect location information in interactive workflows, e.g., when commenting alarm messages but not re-running the analysis.

• RuleChecker configurations can now be expressed in a flexible, more powerful manner. Instead of simple lists of files to check, the tool now supports lists of files and folders to include in or exclude from rule checking.
• Improved performance of rule checking phases if only diagnostic rules (rule sets A and B) are enabled.
• The new option keep-ctype-for-constants allows using the real type of constant expressions instead of the type of lowest rank. This affects rule checks that consider the underlying/essential type (according to MISRA C).
• The option boolean-type now takes a regular expression instead of a single identifier. This allows the specification of multiple types to consider boolean.
• In the scope of a
  /* RULECHECKER_suppress() */
  or
  /* RULECHECKER_suppress(rules-category) */
  occurrences of an identifier are no longer considered for rule checks that warn about naming collisions (e.g. identifier-unique-* or identifier-significance).
• Fixed message texts for C++ rule violations that refer to pseudo-files (e.g. <stdin>, <built-in>, <command line>).
• Fixed exceptional abort of the analyzer caused by certain non-ASCII file content.

MISRA-C

• MISRA-C:2012 Ed. 3 is now fully incorporated.
• Added support for rule M2012.1.3.
• Full support for the MISRA-C:2012 rule 18.7.

• Rule checks for the following rules are now available without envoking a full Astrée runtime error analysis:

  • M2012.18.2
  • M2012.18.3
  • M2012.18.6
  • M2012.22.2
  • M.17.2
  • M.17.3
  • M.17.6
• Improved the application of MISRA’s essential/underlying type concept to compound expressions (GCC extension).
• The check composite-cast (M2012.10.8) has been split into the checks composite-cast and composite-cast-width, checking either the type category or the type width for conversions on composite expressions.
• Split the check macro-parameter-unparenthesized-expression into the two checks macro-parameter-unparenthesized-expression and macro-parameter-unparenthesized-expression-strict. Macro parameters that are expanded into parameter lists can thus be excluded from checks for rule M2012.20.7.
• Improved precision of the check return-implicit. This removes false alarms for the rules M.16.8 and M2012.17.4.
• Improved precision of the checks for rules M.8.3 and M2012.8.3.
• The rules M.8.10 and M2012.8.7 can now be configured with a regular expression that specifies the names of objects that shall not be reported by the check global-object-scope. For example, providing the argument “main” will prevent the main function from being reported.
• Macros that are defined in the scope of a RULECHECKER_SUPPRESS source directive (e.g. in stub libraries shipped with the tool), no longer contribute to the check max-macros-defined for rule M.1.1.

SEI CERT Secure C

• Improved precision of the check return-implicit. This removes false alarms for rule CERT.MSC.37.
• The rules CERT.DCL.15 und CERT.DCL.19 can now be configured with a regular expression that specifies the names of objects that shall not be reported by the check global-object-scope. For example, providing the argument “main” will prevent the main function from being reported.
• Added the check return-reference-local for checking part of rule CERT.ARR.30 without runtime error analysis by Astrée.
• Rule checks for the following rules are now also available without runtime error analysis by Astrée:
  • CERT.ARR.36
  • CERT.DCL.30
  • CERT.MEM.34

CWE

• Added support for the following CWE rules:

  • CWE.467
  • CWE.468
  • CWE.481
  • CWE.558
  • CWE.562
  • CWE.676
  • CWE.825
• Rule checks for the following rules are now available without runtime error analysis by Astrée:
  • CWE.415
  • CWE.761

Other rule sets and checks for C

• The checks static-object-name and static-object-name-const are now restricted to objects of file scope.
• Added new checks local-static-object-name and local-static-object-name-const to check the naming of local objects with static storage duration.
• The check switch-clause-break no longer warns about switch clauses that are terminated by a continue or return statement. Such clauses are now reported by the new checks switch-clause-break-continue and switch-clause-break-return.
• Improved precision of the check function-return-unused when checking compound expressions (GCC extension).
• _Static_assert() with a non-constant expression as condition now triggers a violation of diagnostic rule A.1.6 instead of an error.
• Extended the checks member-name-reuse, identifier-unique, identifier-unique-macro, identifier-unique-typedef, and identifier-unique-extern to unnamed struct/union types and their members.
• The check expression-statement-dead has been split into the checks expression-statement-dead and expression-statement-pure. The latter considers only expression statements which have a function call as a sub-expression, while the former considers all other expression statements.
• The rules X.B.4.6 and X.B.5.5 can now be configured with a regular expression that specifies the names of objects that shall not be reported by the check global-object-scope. For example, providing the argument “main” will prevent the main function from being reported.
• Rule checks for the following rules are now also available without runtime error analysis by Astrée:
  • ISO17961.addrescape
  • ISO17961.dblfree
  • ISO17961.ptrobj
  • ISO17961.xfree
  • X.A.5.60
  • X.A.5.61

Rule sets and checks for C++

• Added support for MISRA rule classification (required, advisory) to the C++ rule sets M2008 and AUTOSAR.
• Rule T.16.1 (check max-size-of-statement) is now also checked on C++ code.
• Removed false alarms for check definition-duplicate and improved context information of rule violation alarm.
• Extended the check member-function-missing-const to warn in additional cases.
• Sharpened the check non-standard-escape-sequence to warn about more non-standard escape sequences.
• Fixed an issue that could cause rule checking to abort with an error while checking single-use-pod-variable.
• Improved type information displayed for rule violations regarding non-compliant type conversions in C++.

• The following code metrics are now available for C++ code:

  • CALLS (# of called functions)
  • CALLING (# of functions calling a function)
  • CDFILE (comment density of a file)
  • CYCL (cyclomatic complexity)
  • FILES (# of original source files)
  • FUN (# of function definitions)
  • GOTO (# of goto statements)
  • LEVEL (nesting depth of control structures)
  • LINE (# of source lines)
  • LOCVAR (# of local variables)
  • LSCOPE (Language Scope)
  • MLINE (# of maintainable code lines)
  • PARAM (# of parameters)
  • PATH (# of execution paths)
  • PLINE (# of physical source lines)
  • RETURN (# of return statements)
  • RPATH (# of recursive paths)
  • STMT (# of instructions)
  • SoS (size of statement)

New diagnostics

• A.2.19 (check enumerator-value)
  warns about enumerators exceeding the range of signed int.
• A.2.20
  warns about the use of compiler built-in functions that are directly supported by the C frontend of Astrée and RuleChecker.
• A.1.13
  warns about a non-standard use of the alignment specifier _Alignas.
• A.2.21
  warns about the use of the compiler-specific type specifier __packed__.
• Added new diagnostic rule checks for former notification messages:
  • A.5.4 (annotation-insertion-failed, conflicting-absolute-addresses, missing-rulechecking-phases)
  • A.1.12 (return-empty, return-non-empty)
  • A.2.17 (empty-struct)
  • A.2.18 (pointer-arithmetic-void)
• Warning messages issued by the Clang frontend are now reported as violations of the new diagnostic rule A.6.2 (clang-warning).
• Syntax and invalid argument errors in Astrée and RuleChecker directives within source code comments, i.e. in comments of the form /* ASTREE_... */ or /* RULECHECKER... */ are now reported as violations of the diagnostic rule A.5.1.
• The new rule set B contains optional Informational Diagnostics, which raise alarms for behaviors of the runtime error analysis (Astrée) that may need to be reviewed depending on the properties of the analyzed code and the chosen analyzer options. The checks in this set replace former notification messages triggered by analyzer options.
  • B.1.1 (ignored-volatile)
  • B.1.2 (unused-suppress-directives)

Stub libraries, ABIs, and compiler configurations

• Modified the generic 32-bit default ABI of the analyzer to assume 8 bytes for size and alignment of long double.
• Added an ABI configuration for Renesas RH850 with Grenhills compiler.
• Corrected the isnormal and signbit macros in the example stub implementation of the C library (math.h).
• The implementation of the macros isfinite, isinf, isnormal, and signbit (math.h) in the example stub implementation of the C library is now compatible with MISRA. This removes alarms about MISRA rule violations when using these macros.
• Modifications of the ABI option wchar_t now affect the WCHAR_MAX and WCHAR_MIN macros provided by the C stub library implementation.
• The libcxx stub library now provides macros that establish a unified interface to the subset of Astrée directives that is available in C, as well as in C++ analysis projects. For example, __ASTREE_CXX_assert(x) is equivalent to __ASTREE_assert((x)). C files using the new macros can be analyzed in C (astree mode) as well as in C++ (astree-cxx mode) analysis projects.
• The stub implementations of the CompCert built-in functions __builtin_fnmadd and __builtin_fnmsub are now provided in a platform-specific way. This fixes the semantics for the x86 target.
• The stub implementation of the CompCert built-in function __builtin_bswap64 is now available for all targets.
• Renamed the CompCert specific ABI configurations to match the naming convention that is used for all other targets. For example, the ABI configuration compcert_x86_32.dax is now x86_32_compcert.dax.
• Added new ABI and compiler configuration for CompCert on PowerPC 32 with the Windriver Diab tool chain.
• Improved the type-generic macros in the tgmath.h header.

Integration with TargetLink

• Added support for Replaceable Data Items.
• The option substitute-functions is no longer overwritten by the TargetLink importer. Instead, the substitutions are now appended.

AUTOSAR support

• Improved automatic AUTOSAR OS configuration from AUTOSAR 3.2 ARXML files. The generator now detects the number of cores.
• The ARXML import for AUTOSAR OS has been extended to support more than 64 events with event mask AUTO.
• The Data flow view for AUTOSAR projects now also displays the involved application and core for each access to a variable. Additionally, variables are classified as process-local, application-local, core-local, or global. The extended information is also available in custom report files.
• The control flow view for AUTOSAR projects now also displays the application and core involved in a function call.

OS configuration

• ARXML files used for OS configuration are now uploaded as "original source" files.
• OIL and ARXML files for OS configuration are now automatically excluded from rule checking.
• Added support for ARXML files that explicitly specify the RES_SCHEDULER resource.
• Fixed an issue that could cause the analyzer to stop with an exception.

Further changes

• The following options have been replaced by the new diagnostic rule checks in rule set B (see the Checks and rules section of these notes):
  • dump-unused-suppress is now B.1.1 check unused-suppress-directive
  • warn-volatile-ignore is now B.1.1 check ignored-volatile
• The option warn-undef-functions has been removed from the interface.
• Repeated __ASTREE_volatile_input directives are now reported as invalid and the duplicate directive is ignored.
• Improved stability of the program slicer when computing context sensitive slices of asynchronous programs.
• The behavior of the option continue-on-definite-rte has been fixed for the analyzer built-in functions __astree_stop_process (when applied to the current process) and __astree_chain_process. These directives will now stop the execution for the current process, even when the option continue-on-definite-rte is set.
• Fixed an issue that could cause the analyzer to crash when enabling at the same time the options exclude-signed-in-unsigned-overflows, separate-with-caller-stack-pointers, and octagon.
• Assigning the address of a variable to a variable with a globally asserted range (specified by __ASTREE_global_assert) now triggers an assertion failure. The analyzer then continues the analysis without considering the assigned address as a possible value for the asserted variable.
• Clarified the alarm message for memcpy, bzero, access, and trash operations with non-integer or too large size arguments. The message now explicitly states the assumption under which the analysis is carried on:

  ALARM (A): ignoring invalid memory operation with non-integer or too large size argument at ...

• Automatic loop unrolling is now available in astree-cxx mode for analyzing C++ code.
• Analysis projects constructed by the scenario builder tool now also inherit rule configurations from their parent project.
• Exported AIS files (option ais-export) now also contain function pointer calls from asynchronous processes.
• Fixed an issue that could cause the analyzer to stop with an exception when the interpolation domain was enabled.
• Improved the Boolean packing heuristic. In particular, it now uses the regular expression specified by the option boolean-type to decide whether a type is Boolean. Additional types may be specified using the new option pack-boolean-types.
• Enabling the option dynamic-smash-variables-threshold no longer smashes variables that differ with respect to the const qualifier. This modification ensures that “write to constant” alarms are issued consistently if the option is enabled.

Qualification Support Kits (QSKs)

• The Safety Manual has been extended with ISO-26262 V2.
• QSK execution now validates all input and output XML files.

New test cases in the Astrée QSK

The test cases qk_option_warn_undef_functions, qk_option_warn_volatile_ignore, and qk_option_dump_unused_suppress have been removed from the Astrée QSK.

New test cases in the RuleChecker QSK