Astrée and RuleChecker release 19.04

Spectre vulnerability detection

Astrée now detects and reports Spectre v1, Spectre v1.1, and SplitSpectre vulnerabilities.
The detection is disabled by default and can be enabled via the new option detect-spectre.

Taint analysis

Astrée can now track taint information for memory locations. This new feature can be used for analyzing security properties. It is disabled by default and can be enabled by setting the option track-taint-hues. Additionally, the new directives __ASTREE_taint and __ASTREE_taint_sink can be inserted into the code for expressing where variables are tainted and which memory locations must not be reached by taints.

Extended AUTOSAR support

• RuleChecker can now check C++ code for compliance with AUTOSAR C++ coding rules as defined in the AUTOSAR document “Guidelines for the use of the C++14 language in critical and safety-related systems”.
• Astrée now supports AUTOSAR multi-core systems using a multi-core aware OS model with support for spinlocks. The OS setup can be automatically derived from ARXML.
• To improve the analysis performance for AUTOSAR projects, Astrée now provides analysis stubs for the AUTOSAR modules NvM (NVRAM Manager) and Dem (Diagnostic Event Manager). The stubs are located in the AUTOSAR subdirectory of the installation, and the user manual now includes a chapter dedicated to their use and configuration.
• It is no longer necessary to manually add __ASTREE_smash directives to prevent smashing on arrays in the generated AUTOSAR OS stubs. The necessary directives are now automatically generated.
• A new define __ASTREE_PHASE_CORE_INIT_TASK can be set in the AUTOSAR preprocessor configuration for analyses of multicore projects with phases. This define causes core initialization tasks to be executed in the first (initialization) phase.

Closed beta: Astrée for C++

This is the first Astrée release to offer static run-time error analysis of C++ code. Evaluation licenses can now be issued on request.

Analysis of finite-state machines

This release introduces a new relational domain for a more precise analysis of finite-state machines.

The new domain is activated with the option state-machine=yes and reacts to the new directive __ASTREE_states_track((x)) which indicates that x is used to encode the state of a state machine.

Special treatment stops upon encountering either __ASTREE_states_merge((x)) or __ASTREE_states_merge(()).

The new option automatic-state-machine=yes enables automatic detection of code patterns used in state machine implementations, for which Astrée can then insert __ASTREE_states_track directives.

Frontends

• The C frontend now accepts lvalue casts, as supported by older versions of the GCC compiler. Example:

  float* fp = 0;
  int* ip = 0;
  (int*)fp = ip; /* lvalue cast */

  Note that such code violates the diagnostic rule A.2.6 (check lvalue-cast) and is no longer supported by current C compilers.
• Source directives are now also accepted and applied in single-line comments (//...).
• The C frontend now rejects strictly invalid array index expressions (which are also not accepted by compilers).

Options

• New option continue-on-definite-rte. If Astrée encounters a definite run-time error while this option is enabled, the analysis does not stop for the affected context but carries on with partial statement semantics.
• New option collapse-multi-dimensional-arrays that controls whether multi-dimensional arrays are considered as a single type layer for naming rule checks.
• The type name configured via option boolean-type is now equivalent to _Bool for naming checks.

Command-line options

• The server broadcast can now be limited to the local host. The feature is available via the server controller and the new server command-line option --local-broadcast.
• Corrected the behavior of the option --export-preprocessed such that it exports the successfully preprocessed files even when the preprocessing of other files fails.

Directives

• Modified the syntax of the following directives to improve consistency:

  New syntax	Old syntax
  __ASTREE_volatile_input((v; [l,h]));	__ASTREE_volatile_input((v, [l,h]));
  __ASTREE_global_assert((v; [l,h]));	__ASTREE_global_assert((v, [l,h]));
  __ASTREE_known_range((v; [l,h]));	__ASTREE_known_range((v, [l;h]));
  __ASTREE_partition_ranges((g; [l,h], [l,h]));	__ASTREE_partition_ranges((v: [l;h], [l;h]));

  The old syntax is still accepted, but the new syntax is now preferred.
• For loops that contain __ASTREE_partition_begin directives, the analyzer is now much faster, thanks to improved widening.
• Astrée can now track taint information for memory locations. This feature can be enabled by setting the option track-taint-hues. Additionally, the new directives __ASTREE_taint and __ASTREE_taint_sink can be inserted into the code for expressing where variables are tainted and which memory locations must not be reached by taints.
• Fixed an issue in the evaluation of the directive __ASTREE_partition_control((1)). Using it in front of a loop caused the first partition to get lost.

ABI

• Renamed the ABI option key endianess to endianness.
• Removed the ABI option rounding_mode_for_constants. Floating point constant expressions evaluated at compile-time are now always evaluated using rounding to nearest (as required by the C standard, see ISO/IEC 9899:2011, F.8.2).
• The default ABI assumed by Astrée and RuleChecker now uses bitfield_sign=signed. The default ABI is now also available as a DAX file (default_generic_32.dax) installed with the other ABIs.
• The analyzer now also considers the ABI option bits_of_byte when determining the size of floats and doubles. (In previous releases it only had an effect on integer types.) Therefore with sizeof_double=4 and bits_of_byte=16 the analyzer now considers doubles to have 64 instead of only 32 bits.
• Fixed essential typing of constant expressions in case that the ABI value bits_of_byte is set to a value other than the default of 8. This affects most M2012.10.x checks, if the ABI is configured in the aforementioned way.
• Fixed the ABI for the Diab compiler on 32-bit PowerPC by setting the ABI option alignof_char_array to its default value of 1. The ABI for this target, as shipped with previous Astrée releases, assumed an alignment of 4, corresponding to the compiler documentation. To the best of our knowledge, this alignment is not used by the compiler for aligning arrays in structs, which is the only case for which the aforementioned option is relevant for Astrée. In such cases the compiler uses a 1-byte alignment.

DAX

• Incremented the DAX version number to 1.6.
• File names in RuleChecker configurations are now exported to DAX using relative paths.
• Improved license-token handling when importing a DAX file containing an <id> tag. The rulechecker token is now released after preprocessing.
• DAX files are now rejected with an error message if they contain the option

  <relational>no</relational>

  followed by

  <any-relational-domain>yes</any-relational-domain>

  where any-relational-domain is the option key of any relational domain, e.g. octagon. In previous releases, such specifications were accepted but led to disparate behaviors in GUI and batch mode.
• Setting the DAX export option Options=All no longer exports sub-options that are disabled by their parent option. This modification ensures that exported DAX files are always consistent with respect to the analyzer options.

Alarms, messages and warnings

• Fixed the display and reporting of unreachable if statements that are partitioned by an __ASTREE_partition_control directive.

Improved reporting

• HTML report files now contain a table of contents for easier navigation in large report files.
• When printing analyzer options to report files, analysis runs in batch mode now behave the same as in GUI mode, i.e. only options that deviate from their default values are now reported.
  To complement that, a new option print-all-options=yes is introduced that forces the printing of all analyzer options, including those set to their default values. It can be used in either mode.
• Functions that are ignored due to an __ASTREE_ignore directive are now displayed as filtered in the editor view.

Server and server controller

• Improved server stability.
• Analyses that fail to start from the server’s analysis queue are no longer automatically re-queued. This fixes issues with queued analysis projects blocking the server.
• Fixed an issue in the installer that prevented the server from starting automatically after reboot, even if the installer option “Register a3 for C server as a service” was enabled.
• The server controller now displays its build number in the title bar.
• The Management view of the server controller now shows the version information of the currently selected server.
• The server broadcast can now be limited to the local host. The feature is available via the server controller and the new server command-line option --local-broadcast.
• The server port can now be configured in the server controller if not restricted by the license file. The last configured port number is used automatically when restarting the server.
• Allow the server to accept command line arguments specified in the Windows service configuration if run as service.

Client GUI and batch mode

• Improved search:
  • Faster filtering and searching in large collections of findings, e.g. in the Findings view.
  • The identifier search no longer lists declarations of objects for which a definition exists. For such objects only the definition is listed. This change improves the performance of the identifier search on very large analysis projects.
  • A search feature that can be invoked by pressing Ctrl+F is now available in all of the following tabs of the Results view: Findings/C, Findings/F, Rule violations, and Reachability.
• Improved performance when displaying source files with large numbers of alarms.
• Fixed the Watch view for investigating variables and lvalues in Astrée. The feature was not working correctly in release 18.10.
• Jumping to another code location or switching from an editor to another view now always enables the button for going back to the last code location.
• The context menu entries "Disable", "Go to annotation" and "Edit" in the editor now also work for AAL-inserted comment directives.
• Fixed the Verbosity selector of the Output view. In release 18.04 and later, changing the verbosity in an already opened analysis project could have undesired effects: empty cells in the 'Message' column of the Findings view missing information (message texts and data races) in XML and custom report files that were generated after modifying the verbosity slider.
• Corrected the behavior of the option --export-preprocessed such that it exports the successfully preprocessed files even when preprocessing of other files fails.
• Hovering over an AAL annotation in the Editor view now also shows the comment for that annotation.
• The Annotations view now allows duplicating a set of annotations.
• Copying contents from the Annotations view into the clipboard now also copies the information if an annotation was disabled.
• The effects of parser filters are now displayed immediately after the frontend has finished and before starting the analysis.
• List edit dialogs for complex options now also allow editing the list of parameters in a text edit field.
• The split view for preprocessed code now provides context menu entries for jumping to the corresponding line in the original code editor. The feature is available in the preprocessed code editor as well as in the associated original code view on the right-hand side.
• Fixed display of the "Definite runtime error" line in the detailed call stack information area of the Findings view which was missing in 18.10i releases.
• Fixed an issue with the display of lengthy tooltips in editor views.
• Fixed an issue that caused coverage, data flow, and control-flow information to be missing from the predefined report files in batch mode.

Improved precision

• Precision has been improved for all of the following checks:
  • address-of-overload
  • digraph-token
  • stdlib-use
  • unrelated-pointer-conversion
  • unary-assign-separation
  • virtual-call-in-constructor
  • return-position
  • inconsistent-default-argument
  • null-as-integer
  • multiple-loop-counters
  • mixed-virtual-base
  • member-function-missing-const
  • controlling-invariant-expression
    used in rule M.14.1, M2012.2.1, and M2012.14.3
  • parameter-missing-const
    for rule CERT.DCL.0, CERT.DCL.13, M.16.7, and M2012.8.13
  • wide-narrow-string-cast and
    wide-narrow-string-cast-implicit
    used in rule CERT.STR.38
• Improved precision of the check plain-char-usage in code using the comma operator or references.
• Improved precision of the check underlying-cvalue-conversion by ignoring irrelevant implicit conversions, like "non-const" to "const" pointers.

Improved placeholders

• Naming-rule configurations can now use the new placeholder %Module_abbreviation%. The expansion of the placeholder, e.g. xyz, is defined per source file using the syntax \module_abbreviation xyz in an arbitrary comment.
• Fixed evaluation of the placeholder %Folder#% which was ignored in all 18.04i and 18.10 builds.
• The placeholder %bitsize% is now also available for objects of struct or enum type, including enumeration constants.

Other improvements

• New option collapse-multi-dimensional-arrays that controls whether multi-dimensional arrays are considered as a single type layer for naming rule checks.
• The type name configured via option boolean-type is now equivalent to _Bool for naming checks.
• Pragmas of the form

  #pragma push_macro("XYZ")
  #pragma pop_macro("XYZ")

  are no longer rejected with an error message if XYZ is not defined.
• In case of errors during parsing, RuleChecker now always terminates with exit code 1, after performing partial rule checking on the successfully parsed files.

New rules for C

• T.15.1, associated with the check max-local-variables.
  This check is violated if the specified threshold for local variables in a function is exceeded.
• T.16.1, associated with the check max-size-of-statement.
  This check is violated if the specified threshold for the sum of operands and operators in a statement is exceeded.

Rule sets and checks for C

• New rule check multiple-writes-in-full-expr warns about full expressions in which a variable is written more than once. This is used to warn about violations of rule M.12.2.
• New diagnostic rule A.1.11 warns about implicit conversion between incompatible pointer types.
• Extended coverage of rule M.1.1, M.11.1, M2012.1.1, M2012.11.1, and CERT.MSC.40.
• Removed false alarms for:
  • pointer-qualifier-cast-const-implicit when the second argument to __astree_memcpy is a pointer to const
  • boolean-invariant in switch statements
  • multiple-volatile-accesses and evaluation-order when they take the address of an array
  • array-initialization (rule M2012.9.3) in case of nested arrays inside of zero-initialized structures, such as
    struct { int a[2];} s = { 0 };
• The check function-pointer-cast for rule M.11.1 and M2012.11.1 no longer warns about null pointer constants.
• The following checks have been split for const-qualified and non-constant objects:

  global-object-name	↗ ↘	global-object-name global-object-name-const
  static-object-name	↗ ↘	static-object-name static-object-name-const
  local-object-name	↗ ↘	local-object-name local-object-name-const

• Fixed essential typing of constant expressions in case that the ABI value bits_of_byte is set to a value other than the default of 8. This affects most M2012.10.x checks, if the ABI is configured in the aforementioned way.
• Alarms concerning essential types now also mention the type, not just the category.
• The option allow-signed-constant-with-unsigned is now also considered for the check bitop-type used in rule CERT.INT.13, CERT.INT.16, M.12.7, and X.A.5.
• The check integral-type-name, used in rule M.6.3, M2008.3.9.2, M2012.D.4.6, X.A.5.6, and X.D.8.2.a, now honors the exceptions 2, 3, and 4 of MISRA-C:2012 directive 4.6. Therefore, it no longer warns about uses of the predefined types int and char in a declaration or definition of the main function.
• Diagnostics rule A.5.2 now also warns about #pragma directives whose semantics are not taken into account by Astrée.

SEI CERT Secure C

Added support for following SEI CERT coding rules/recommendations:

• CERT.EXP.5
• CERT.EXP.9
• CERT.EXP.13
• CERT.EXP.15
• CERT.EXP.16
• CERT.INT.16

• CERT.PRE.11
• CERT.PRE.12
• CERT.PRE.30
• CERT.STR.5
• CERT.STR.10

• CERT.API.8
• CERT.ARR.1
• CERT.ARR.39
• CERT.DCL.5
• CERT.ERR.7
• CERT.WIN.1

Rule sets and checks for C++

• New checks:
  • multiple-writes-in-full-expr warns about full expressions in which a variable is written more than once to warn about violations of rule M2012.13.2.
  • float-suffix for rule M2008.2.13.4 warns about the floating literal suffix 'f'.
• The check functional-cast no longer reports constructor conversions.
• The checks new-operator and delete-operator no longer warn about placement operators.
• The check unary-assign-separation is now also applied to overloaded operator calls.
• The checks for rule M2008.6.4.3 no longer warn about switch statements without default clause.
• The checks for rule M2008.6.4.6 no longer warn about exhaustive switch statements over values of enum type without default clause.
• Improved the check functional-cast for rule M2008.5.2.4.
• Sharpened the check bitop-type to warn about more cases of bit operations on values of unfitting type.
• The check cast-integer-to-pointer now warns about casting an integral type to any pointer type.
• The check integral-type-name now also warns about uses of integral type names in cast operators.
• Rule M2008.7.3.1 can now be parameterized with a set of type names that are allowed to be declared at file scope.
• Improved the check for rule M2008.8.5.2 to eliminate false alarms for empty initializer lists initializing the whole object, e.g.
  int a[2][2] = {}; // compliant.
• The check unused-internal-function (rule M2008.0.1.10) no longer warns about template functions.
• The check float-bits-from-pointer (rule M2008.3.9.3) now also covers reinterpret_cast.
• The check enum-usage (rule M2008.4.5.2) no longer warns if the unary & operator is applied to an expression of type enum.
• Refined checks for rule M2008.4.5.3.
• Improved the check loop-control-modification for rule M2008.6.5.5.
• Improved the check inappropriate-enum for rule M2012.10.1 to eliminate false alarms for expressions of the form &arr[e] when e is of enum type.

AUTOSAR C++ support

New rule set “AUTOSAR” with checks for AUTOSAR C++ coding rules as defined in the AUTOSAR document “Guidelines for the use of the C++14 language in critical and safety-related systems”.

Metrics

• The new function metric LOCVAR counts the number of local variables which are declared in a function.
• The LSCOPE metric now considers all function calls, dereferences, array look-ups and struct-member accesses.

Stub libraries and compiler configurations

• To improve the analysis performance for AUTOSAR projects, Astrée now provides analysis stubs for the AUTOSAR modules NvM (NVRAM Manager) and Dem (Diagnostic Event Manager). The stubs are located in the share/source/AUTOSAR subdirectory of the installation. The use and proper configuration of these stubs is described in the user manual.
• Modified the OSEK stub generation from .oil files, so that ISRs may now preempt tasks which hold the scheduler resource (RES_SCHEDULER). Please note that this modification only affects analyses which are configured to take priorities precisely into account (precise-priorities=yes). With the default option 'precise-priorities=no' the analyzer does not exclude preemption based on resource priorities.
• The compiler configuration and stub library for CompCert PowerPC has been extended to support the built-in functions isel64, uisel64, and bsel, provided by recent versions of the compiler.
• Fixed the ABI for the Diab compiler on 32-bit PowerPC by setting the ABI option alignof_char_array to its default value of 1. The ABI for this target, as shipped with previous Astrée releases, assumed an alignment of 4, corresponding to the compiler documentation. To the best of our knowledge, this alignment is not used by the compiler for aligning arrays in structs, which is the only case for which the aforementioned option is relevant for Astrée. In such cases the compiler uses a 1-byte alignment.

Preprocessor

• C, C++, and other stub-library include paths have been moved to the end of the include-path list. This allows to provide custom standard header replacements if needed. For example, a math.h of your own will now overwrite the stub library math.h shipped with the tool.
• The C99 macro __TIME__ now expands to ??:??:??, and likewise __DATE__ now expands to ??? ?? ????. This ensures stable results between different analysis runs.

Slicing

Context proposals for program slicing no longer contain contexts that have not been reached by the runtime error analysis.

License management

• Improved the ALM token handling for cases when the connection between the analysis client and the analysis server is lost during preprocessing. The rulechecker token is now immediately released as soon as the server considers the connection definitely lost.
• Improved the ALM token handling in case of importing a DAX file that contains an <id> tag. The rulechecker token is now released after preprocessing.

Integration with TargetLink

• Added support for the new TargetLink release 4.4.
• The AbsInt toolbox for TargetLink can now be configured to run the analysis in batch mode instead of running it in GUI batch mode. The analysis then runs without any user interaction and without opening any windows.
• Improved precision of the interpolation domain. If activated, the analyzer now reports significantly fewer alarms in TargetLink interpolation functions.
• Removed unintended output (state = 'Hidden') from the Matlab command window.
• The AbsInt toolbox for TargetLink and the TargetLink Data Dictionary Importer now provide an option for generating __ASTREE_partition_control directives instead of __ASTREE_unroll directives for interpolation routines.

Other Astrée improvements

• When the second argument of a shift is too big (raising the alarm “range of second shift argument ... not included in ...”), the analyzer now also includes 0 in the result.
• Alarms about possible data races now include the name of the process in which the alarm is detected.
• The analyzer no longer stops with an error if the return type of a function is not compatible with the return type assumed by the calling expression and the result of the function call is not used. Instead, the analysis raises an alarm A and continues. The new behavior is consistent with the behavior for incompatible function calls in which the result is used by the caller.
• Improved the analyzer's precision on computations with bit-masks.
• The heuristic selection of functions for context-insensitive analysis (option separate-function=*) now takes function substitutions into account. This results in a better choice of separate functions in the presence of function substitutions.
• Improved analyzer performance for analysis projects that enable the option warn-on-field-overflows.
• Improved the precision of location information for certain alarms. In particular write data race and global assertion alarms in an assignment are now reported for the left-hand side of the assignment. Please note that comments for such alarms may need to be moved to the new location when re-running older analyses.
• Fixed false alarms in __ASTREE_modify directives on arrays.
• For function calls with incompatible parameter or return types, the analyzer now assumes that values with incompatible type are converted according to the rules of C, if such rules are applicable. Otherwise it assumes any value.
• Fixed address computation for objects that are specified to overlap in memory by __ASTREE_absolute_address directives.
• Control flow information is now also displayed if the reporting of data flow information was disabled for the analysis (using the option dump-dataflow=no). Moreover, it now also contains call information for calls that are only reachable via separately analyzed functions (option separate-function).
• Function calls with incompatible types now always raise an alarm of type A. Previous releases raised an alarm of type A or C depending on the kind of incompatibility.
• Added new analyzer intrinsic functions for simplified process creation. After invoking __astree_create_process with minimal arguments, the following functions can be called for setting further process properties:
  • __astree_set_process_running_priority(process_id, priority)
  • __astree_set_process_non_realtime(process_id)
  • __astree_set_process_core(process_id, core)
• Added the new analyzer-intrinsic function __astree_core_process(unsigned *c) which stores in *c the ID of the core that the current process is running on.
• Improved the performance of the static dependencies pre-analysis.
• Fixed an issue in the gauges abstract domain that could remove some traces from the analysis, possibly stopping the analyzer with an error message.
• Fixed an issue that caused the analyzer to abort with an error message when using an undeclared absolute address of with an incomplete type, e.g.

  struct T {}; // incomplete type ...
  struct T* p = (struct T*)0x1000; //  ... used with absolute address

• Fixed an issue that in rare circumstances could stop the analyzer with the error message "Cannot project mismatching partition IDs".
• Fixed an issue that caused the analysis to abort with an error message in a function call with incorrect type. After reporting the error, the analyzer now proceeds, assuming that the value of the incorrectly typed argument is undefined.
• Fixed an issue with missing data-race alarms in case that a low priority process writing to a variable could be interrupted by a higher priority process reading from the same variable and the option precise-priorities=yes was set. Please note that the effects of the data race were soundly taken into account by the analyzer, so that possible run-time errors triggered by the data race were still reported. The fix only ensures that the analyzer reports the additional data race alarms in this situation.

Other changes

• The tool now uses more descriptive names when referring to static variables whose identifier is not unique. For example, a static variable named var and declared in file.c is now reported as var@"file.c".
• Multiple files with the same file name are now distinguished by adding the minimum path information required for obtaining a unique name. Elided prefixes are represented by a single ‘...’. For example, the files

  /test/share/libcxx/include/stdlib.h
  /test/testcase/stubs/stdlib.h

  are now represented as

  .../include/stdlib.h
  .../stubs/stdlib.h

  The short files names are used in the analyzer output as well as in the text and HTML report files.
• Analysis queuing is now fully supported for both Astrée and RuleChecker analyses.
• The import of external declarations from text format (*.edf) is no longer supported.

TOR/VTP improvements

• Added the sub words REQ and QK to the legend for the construction of requirement/test case identifier names.
• Only the configuration recommendations relevant to the particular core feature are now shown in the TOR.
• Avoiding usage of the abbreviation “QSK” without explanation.
• Added a section listing the covered D0-330 objectives.

Other improvements

• Enhanced check for Windows’ max path limitation.
• Revised QSK package file names and improved installation path consistency checks.
• Added missing text fragments to the Verification Test Plan for RuleChecker concerning the QSK tests qk_check_extra_tokens and qk_check_non_standard_identifier.

New test cases in the Astrée QSK

The test case qk_abi_rounding_mode_for_constants has been removed from the Astrée QSK.

New test cases in the RuleChecker QSK