Astrée Release 20.04

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

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.

RuleChecker

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

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:

<substitute-functions>a=b,c=d</substitute-functions>
<separate-function>f,g<separate-function>

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

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 alex@absint.com. Copyright 2020 AbsInt.
------------------------------------------------------------------------------
An HTML version of these release notes is available at
absint.com/releasenotes/astree/20.04