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 and for conditional returns.

  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.

  New options

▲ The new option warn-on-tainted-control-flow enables additional alarms
  if tainted values with specified hues reach control flow decisions.
▲ The new option cut-write-to-const configures the behavior of 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

▲ 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_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.

  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

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


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

  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.

  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 
▲ Improved the context information provided with alarms about violations 
  of rule M2008.2.10.1 and AUTOSAR.2.10.1M.


  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


  Added support for rule M2008.5.0.10.

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

    <!-- DAX version >= 1.9 -->
      <item key="a">b</item>
      <item key="c">d</item>

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

  Other Astrée features

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

  Further changes to Astrée

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

  New test cases in the Astrée QSK

▲ qk_dax_clibrary
▲ qk_dax_report_file
▲ qk_directive_wrapper_call
▲ 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_cut_write_to_const,
  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_dax_clibrary
▲ qk_dax_path
▲ qk_dax_report_file
▲ qk_directive_comment
▲ qk_directive_suppress
▲ qk_check_enumerator_value
▲ qk_check_empty_struct
▲ qk_check_pointer_arithmetic_void
▲ qk_check_unnamed_parameter
▲ qk_check_constant_expression_extended_pp
▲ qk_check_non_standard_escape_sequence_pp
▲ 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 k_option_clibrary, k_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

Last updated on 30 April 2020 by Copyright 2020 AbsInt.
An HTML version of these release notes is available at