Astrée and RuleChecker release 20.04

Improved precision

• Improved precision when analyzing asynchronous programs.
• Improved analysis precision in loops containing array accesses.
• The built-in program slicer is now more precise for break and goto control flows, as well as for conditional returns.
• Improved analysis precision on comparisons that involve right shifts such as if (x >> 5 >= y).

Improved performance

• Analysis projects with asynchronous processes that used to take many global iterations may now terminate faster.
• Improved widening to ensure termination when the gauge and state machine domains are both activated.
• Improved the efficiency of the gauge domain on certain code patterns.
• Optimized the GUI so that analysis projects open faster.
• Improved performance of results display, in particular for analysis projects with many findings.
• Reduced memory consumption of the C frontend.

Other improvements to Astrée

• Function calls — usually via function pointers — that supply too many, too few, or inconvertible arguments now stop the analysis in affected contexts. Three new options allow fine-tuning the behavior of the analyzer. They configure in which cases the analyzer follows or cuts an invalid function call:
  • cut-calls-with-too-many-arguments
  • cut-calls-with-too-few-arguments
  • cut-calls-with-inconvertible-arguments
• Function calls in analysis wrapper code that intentionally provide too few arguments must use the new __ASTREE_wrapper call directive. It emulates a function call with arbitrary, full range, initialized arguments.
• The directives __ASTREE_print and __ASTREE_alarm can now report value ranges of simple variables as part of the printed string. For example, the following two directives

  __ASTREE_print(("Hello x: %0", x));
  __ASTREE_alarm((raise_here; user_defined; "Bad value: %0", x));

  trigger this output of the analyzer:

  Hello x: [4, 10] at ...
  ALARM (C): Bad value: [4, 10] at ...

• Improved the printing of floating-point numbers in the analyzer output.
• Removed the option print-float-digits.
• The alarm message “Invalid function call: function <name> has unnamed arguments” has been removed. Unnamed parameter declarations are now reported as violations of the new diagnostic rule A.1.14.
• Non-returning function calls are now also reported if the separate-function option is set and the called functions are analyzed context-insensitively.
• Read accesses to uninitialized pointers are now reported with more precise code location. For example, the issue in the following code is now reported for ptr instead of *ptr:

  int* ptr;
  int val = *ptr;

• Reached code statistics now also count statements inside of GCC’s statement expressions.
• Reachable code tables in the text report are now printed in (lexicographic) ascending order of entries.
• Recursive function calls in separate-function contexts may no longer stop the analyzer. Instead it reports the recursion and continues with the analysis after the recursive call.
• The clock domain is now disabled by default. Analysis projects that require this domain need to explicitly activate the clock option.
• The list of lvalues provided to an __ASTREE_modify directive is now evaluated left-to-right, instead of right-to-left. Please note that this may change the semantics of such directives in certain cases. Example:

  __ASTREE_modify((arr[i], i; [5,5]));

• Subtraction of two NULL pointers now raises an alarm.
• Corrected the behavior of analysis runs that enable both options separate-function and separate-with-caller-stack-pointers, and that call separately analyzed functions in analysis contexts affected by state machine partitioning. Such calls are now fully analyzed, instead of stopping the analysis for this trace with the alarm “call never returns”.

New options

• warn-on-tainted-control-flow
  enables additional alarms if tainted values with specified hues reach control flow decisions.
• cut-write-to-const
  configures Astrée with respect to writes to constant memory. If enabled, the analyzer assumes that execution will not continue after such writes.

Server and server controller

• The server controller now supports starting multiple analysis servers on the same machine.
• The server command line options -D and --license-file no longer modify the corresponding settings configured in the server controller.

Frontends and preprocessor

• Reduced memory consumption of the C frontend.
• The include stack printed with error messages of the preprocessor is now linked to the source code. That is, clicking on a line of the form "In file included at ..." now opens an editor view at the position of the #include directive.
• Removed undocumented syntax extensions for the __ASTREE_print directive from the C frontend. Customers that used the extension for alarm printing should replace __ASTREE_print(("msg";check)); with __ASTREE_alarm((raise_here; user_defined; "msg"));
• __ASTREE_partition_control and __ASTREE_max_clock now accept constant integer expressions as arguments.
• Improved reporting of invalid __ASTREE_unroll directives.
• Improved C frontend error message for duplicate type definition.
• The C frontend now supports enum type declarations with __attribute__((packed)).
• AAL annotations can now also be inserted into files containing anonymous global struct or union declarations.
• The C frontend now supports pure extern declarations of type void.
• Fixed an issue that caused the C frontend to abort with exception or to not terminate in presence of recursive functions.
• Removed support for the following, deprecated alternative syntax of Astrée directives:
  • __ASTREE_unroll(()) without argument
  • __ASTREE_partition_ranges((... : [ ... ; ... ] ...));
  • __ASTREE_known_range((... , [ ... ; ... ]));
  Please see the user manual for valid alternatives.
• Corrected the alignment of bit-fields when alignment and size of their underlying types differ, e.g, due to the ABI specification or the use of packed attributes.
• The C frontend now accepts assembler statements of the form asm {...}. Tokens between the braces are ignored and a diagnostic about violation of rule A.2.2 is issued.

Stub libraries, ABIs, and compiler configurations

• Standard library stubs are now enabled by default when creating new analysis projects using the GUI, if the preprocessing tag <clibrary/> is absent from a DAX file.
• All C stub library functions can now be overridden by implementations in user code.
• The values returned by the stub implementations of acosf, asinf, atanf, and atan2f now also cover the extremal values possibly returned by concrete implementations of these functions.
• The function strncpy(dst, src, n); now reads at most n chars from src.
• Added new C standard library stub implementations for fmin, fminf, fminl, fmax, fmaxf, fmaxl, rand, srand.
• Improved the stub implementations of many mathematical C standard library functions by:
  • Handling NaN and +/−∞ inputs and return values, to enable proper use of stubs in conjunction with the analyzer option keep-float-specials=yes
    This affects the stubs acos, acosf, acosh, acoshf, asin, asinf, atan, atanf, atan2, atan2f, cos, cosf, cosh, coshf, ilogb, ilogbf, modf, modff, pow, powf, sin, sinf, sqrt, sqrtf, tan, tanf, ceil, ceilf, erf, erff, erfc, erfcf, fabs, fabsf, floor, floorf, fmod, fmodf, ldexp, ldexpf, remainder, remainderf, rint, rintf, exp, expf, exp2, exp2f, expm1, expm1f, frexp, frexpf, hypot, hypotf, cbrt, cbrtf, logb, logbf, nextafter, nextafterf.
  • Properly handling corner-case inputs and return values (e.g. subnormals), and adding support for negative inputs to nextafter(f) and remainder(f).
    This affects the stubs ceil, ceilf, erf, erff, erfc, erfcf, fabs, fabsf, floor, floorf, fmod, fmodf, ldexp, ldexpf, remainder, remainderf, rint, rintf, cbrt, cbrtf, logb, logbf, nextafter, nextafterf.
  • Improving precision.
    This affects the stubs exp, expf, exp2, exp2f, expm1, expm1f, frexp, frexpf, hypot, hypotf, cbrt, cbrtf, logb, logbf, nextafter, nextafterf.

OS configuration

The generated stubs for AUTOSAR now also handle calls to CallNonTrustedFunction (for MicroSAR ARXML files).

XML report

• The XML report file now indicates whether option values and ABI settings correspond to their defaults. To this end, the <option/> and <abi_option/> tags have been extended by a new attribute is_default="0/1".
• <location/> tags in XML report files now contain additional o_start_col and o_end_col attributes if the location information refers to an original source file only. The values found in the o_file, o_start_line, o_start_col, o_end_line, o_end_col attributes are then identical to those in the p_file, p_start_line, p_start_col, p_end_line, p_end_col attributes. Location tags of this kind are referenced by RuleChecker alarms that are detected directly on the original source code.
• Added a new, optional attribute frontend_deviation to the <abi_option/> tag. The optional attribute is added if the tool detects that frontend and analyzer have been executed with different ABI settings.

Improved handling of annotation insertion errors

• A new dialog gives detailed feedback about causes of Annotation insertion errors.
• Annotations with insertion errors are highlighted using the red error icon. The yellow exclamation mark icon is now used for annotations with findings, as in the Editor view.
• Annotations with insertion errors can be easily removed or re-generated.

Other improvements to the GUI, batch mode, and report file generation

• Optimized the GUI so that analysis projects open faster.
• Improved performance of results display, in particular for analysis projects with many findings.
• Improved user interface for copying and editing alarm classifications and comments in the Findings view.
• In custom report configurations, the alarm classification filter (Results → Findings → Include → Alarms → Classifications) is now also applied to the lists of findings in the "Rule violations" section.
• The Astrée options profile “Setup (fast)” no longer disables the partitioning domain completely. It now only disables automatic partitioning heuristics.
• Fixed “Failed to include oil_generated.h” errors when re-running analyses with OSEK or AUTOSAR OS configuration without preprocessing again.
• User and password for the analysis server can now also be specified using environment variables instead of command line options. In contrast to the latter, using the environment variables hides the user and password from the command line information in report files when starting analyses in batch mode.
• The analysis wrapper generator now generates code that uses the new directive __ASTREE_wrapper_call.
• Added command line options to enable detached batch mode execution and post-analysis report generation in batch mode:
  • --detach
    allows to detach and exit the a3c executable as soon as the analysis start is triggered on the server. In this case, the text report file only contains the preprocessing output.
  • --report-only
    allows to generate the specified report files for a server project specified via the command line options --id and --revision.

Plugin for ARM Keil µVision

The tool installation now provides a plugin for integrating RuleChecker with the ARM Keil µVision IDE/Debugger.
A free video tutorial on installing and using the plugin is available on our YouTube channel.

Rule sets and checks for C

• Support for MISRA C:2012 Amendment 2.
• The new diagnostic rule A.1.14 reports parameter declarations without name at function definitions.
• Improved readability of alarm messages about metric threshold violations (rule set T) and static-assert check failures (diagnostic rule A.1.6).
• Extended the check pointer-arithmetic-void (rule A.2.18) to unary assignment operators ++ and --.
• Violations of the global check max-number-of-recursive-paths are no longer reported at an (arbitrarily chosen) code location.
• Alarm messages about violation of the rule check min-comment-density-his now always include the metric value.
• Fixed rule checking of code with macros that use the defined operator in their expansion, e.g. #define DEF(...) defined(...)
• Added support for GCC’s variadic macro extension. In sequences like

  , ##__VA_ARGS__

  the comma is erased if no variadic arguments are provided.
• Improved reporting of violations of rule M2012.8.5 by displaying pairs of conflicting locations.
• Updated coverage information reported for rules M.16.2, M2012.17.2, X.A.3.11, X.B.3.13, and X.B.4.1.
• Improved checks for rules M.10.1, M.10.3, M.10.5, and M.12.8 on expressions with integer constants of type (un)singed long or (un)signed long long.
• The check bitfield-signed-size no longer produces false alarms if the ABI option bitfield_sign is set to unsigned.
• The new check constant-expression-extended-pp (rule A.2.4) warns about non-standard constant integer expressions in preprocessor directives.
• The new check non-standard-escape-sequence-pp (rule A.2.11) warns about non-standard escape sequences in character literals in preprocessor directives.
• Corrected MISRA rule coverage information reported for rule M.19.15 and M2012.D.4.10.
• The number of characters considered when checking for distinct identifiers can now be configured for all relevant rules, namely CERT.DECL.40, ISO17961.funcdecl, M2012.5.1, M2012.5.2, M2012.5.3, M2012.5.4, and M2012.5.5.

Rule sets and checks for C++

• Metric threshold checks (rule set T) are now available for all C++ code metrics supported by RuleChecker.
• Improved information provided with alarm messages about violation of the check inconsistent-default-argument.
• The check loose-asm now also warns about assembler code in lambda expressions.
• The check null-as-integer (rules M2008.4.10.1 and AUTOSAR.4.10.1M) now supports arbitrary definitions of the NULL macro.
• Improved type information provided in case that the check polymorphic-downcast fails (violation of rule M2008.5.2.3).
• Metric computation now always takes initializer lists into account.
• Improved the checks include-guard-missing, include-position, define-in-block, error-directive, and non-directive to remove false alarms in comment blocks starting with //*.
• Fixed the metrics PLINE and CDFILE for code that contains comments starting with //*.
• The check undefined-extern no longer warns about undefined pure virtual functions. These are now covered by the new check undefined-extern-pure-virtual.
• Improved the context information provided with alarms about violations of rule M2008.2.10.1 and AUTOSAR.2.10.1M.

AUTOSAR

Added support for the following AUTOSAR rules:

• AUTOSAR.3.1.4A
• AUTOSAR.5.0.10M
• AUTOSAR.6.2.2A
• AUTOSAR.6.2.3M
• AUTOSAR.6.4.1A

• AUTOSAR.6.5.3A
• AUTOSAR.7.1.7A
• AUTOSAR.7.1.9A
• AUTOSAR.7.5.1A
• AUTOSAR.7.5.2A

• AUTOSAR.7.6.1A
• AUTOSAR.8.4.8A
• AUTOSAR.8.5.1A
• AUTOSAR.9.3.1A

MISRA C++

Added support for rule M2008.5.0.10.

Other RuleChecker improvements

• An excerpt of the code affected by a rule violation is now also displayed for C++ code.
• RuleChecker now supports the _Pragma preprocessing operator in C.
• The source directives
  • /* ASTREE_suppress(...) */
  • /* ASTREE_comment(...) */
  • /* RULECHECKER_suppress(...) */
  • /* RULECHECKER_comment(...) */
  now also affect violations of the check clang-warning.
• Occurrences of an identifier in a file that is excluded from rule checking are no longer considered for rule checks that warn about naming collisions, e.g. identifier-unique-* or identifier-significance.

Integration with TargetLink

Updated the TargetLink integration to use the new directive __ASTREE_wrapper_call.

New DAX version 1.9

• Changed default value of the preprocessing tag <clibrary/> from no to yes.
• Options that take value or key-value lists as parameters can now be specified in a structured way. Example:

  <!-- DAX version <= 1.8 -->
  <substitute-functions>a=b,c=d</substitute-functions>
  <separate-function>f,g<separate-function>
  
  <!-- DAX version >= 1.9 -->
  <substitute-functions>
    <item key="a">b</item>
    <item key="c">d</item>
  </substitute-functions>
  <separate-function>
    <item>f</item>
    <item>g</item>
  </separate-function>

• Introduced new directives __RULECHECKER_comment((...)); and __RULECHECKER_suppress((...)); as aliases for __ASTREE_comment((...)); and __ASTREE_suppress((...));, respectively.
• Harmonized the log and text report format for alarm and error messages. These messages are now always enclosed in brackets.
• Updated to the LLVM/Clang 10 toolchain.

New test cases in the Astrée QSK

• qk_dax_clibrary
• qk_dax_report_file
• qk_directive_wrapper_call
• qk_option_cut_write_to_const
• qk_option_cut_calls_with_too_many_arguments
• qk_option_cut_calls_with_too_few_arguments
• qk_option_cut_calls_with_inconvertible_arguments
• qk_option_warn_on_tainted_control_flow
• qk_check_invalid_directive

The test cases qk_option_report_file, qk_option_print_float_digits, and qk_alarm_unnamed_argument have been removed from the Astrée QSK.

The test case qk_option_code_line has been renamed into qk_option_code_lines.

New test cases in the RuleChecker QSK

• qk_check_enumerator_value
• qk_check_pointer_arithmetic_void
• qk_check_unnamed_parameter
• qk_check_constant_expression_extended_pp
• qk_check_non_standard_escape_sequence_pp
• qk_check_pure_override
• qk_check_implicit_float_integral_conversion
• qk_check_cast_zero_to_null_pointer
• qk_check_non_boolean_conditional
• qk_check_non_boolean_loop_condition
• qk_check_null_as_integer
• qk_check_bool_in_non_boolean_context
• qk_check_unused_local_typedef
• qk_check_underlying_bitop_width
• qk_check_non_boolean_logop
• qk_check_multiple_loop_counters
• qk_check_virtual_definition_override

• qk_dax_clibrary
• qk_dax_path
• qk_dax_report_file
• qk_directive_comment
• qk_directive_suppress
• qk_check_empty_struct
• qk_check_switch_bool
• qk_rule_a_1_14
• qk_rule_a_2_17
• qk_rule_a_2_18
• qk_rule_a_2_19
• qk_rule_m_16_2

The test cases qk_option_clibrary, qk_option_path, and qk_option_report_file have been removed from the RuleChecker QSK.

Test cases for ABI settings

Some test cases have been renamed for improved consistency:

• qk_abi_alignment_of_*   → qk_abi_alignof_*
• qk_abi_size_of_*        → qk_abi_sizeof_*
• qk_abi_sign_of_char     → qk_abi_char_sign
• qk_abi_sign_of_bitfield → qk_abi_bitfield_sign
• qk_abi_enum_sign        → qk_abi_enum_preferred_sign
• qk_abi_enum_size        → qk_abi_enum_preferred_size

The test cases qk_abi_alignof_attributed_pointers, qk_abi_pointer_attributes, and qk_abi_sizeof_pointer_attributes have each been split into three separate test cases for each individual ABI setting.

The following is the complete list of all test cases for ABI settings that are now new as a result:

• qk_abi_alignof_bool
• qk_abi_alignof_char_array
• qk_abi_alignof_double
• qk_abi_alignof_float
• qk_abi_alignof_function_pointer
• qk_abi_alignof_int
• qk_abi_alignof_long
• qk_abi_alignof_long_double
• qk_abi_alignof_long_long
• qk_abi_alignof_pointer
• qk_abi_alignof_short
• qk_abi_alignof_attributed_pointer_1
• qk_abi_alignof_attributed_pointer_2
• qk_abi_alignof_attributed_pointer_3

• qk_abi_atomic_bool
• qk_abi_atomic_char
• qk_abi_atomic_double
• qk_abi_atomic_float
• qk_abi_atomic_function_pointer
• qk_abi_atomic_int
• qk_abi_atomic_long
• qk_abi_atomic_long_double
• qk_abi_atomic_long_long
• qk_abi_atomic_pointer
• qk_abi_atomic_short

• qk_abi_bits_of_byte
• qk_abi_bits_of_char
• qk_abi_char16_t
• qk_abi_char32_t
• qk_abi_endianness
• qk_abi_enum_preferred_sign
• qk_abi_enum_preferred_size
• qk_abi_intmax_t
• qk_abi_intptr_t
• qk_abi_pointer_attributes_1
• qk_abi_pointer_attributes_2
• qk_abi_pointer_attributes_3
• qk_abi_ptrdiff_t
• qk_abi_rounding_mode
• qk_abi_sig_atomic_t
• qk_abi_bitfield_sign
• qk_abi_char_sign
• qk_abi_unaligned_dereference
• qk_abi_wchar_t
• qk_abi_wint_t

• qk_abi_sizeof_bool
• qk_abi_sizeof_double
• qk_abi_sizeof_float
• qk_abi_sizeof_function_pointer
• qk_abi_sizeof_int
• qk_abi_sizeof_long
• qk_abi_sizeof_longlong
• qk_abi_sizeof_pointer
• qk_abi_sizeof_short
• qk_abi_size_t
• qk_abi_sizeof_attributed_pointer_1
• qk_abi_sizeof_attributed_pointer_2
• qk_abi_sizeof_attributed_pointer_3
• qk_abi_sizeof_long_double