Astrée and RuleChecker release 18.10

Eclipse plugin

An Eclipse plugin for Astrée and RuleChecker is now available and included in the installation package.

Improved performance

• Astrée analyses are now significantly faster, and use considerably less memory. This is especially noticeable for:
  • combine operations
  • the context-insensitive analysis in sequential code
  • widening operations for common code patterns (disabled special handling for linked lists)
• Significantly reduced the time needed to open analysis projects with large data flow information.

Higher precision

Astrée is now more precise when analyzing interpolation functions, in particular code generated by the TargetLink code generator for Matlab.

Improved RuleChecker

• Improved performance for large C++ projects.
• Identifier search on original source files, including C++ files. This is now the default search mode for the operation “Find in project” in all editors.
• Support for #pragma once.
• Support for #include_next, __has_include(), and __has_include_next().
• Improved support for source files without a file extension. File names like inc.folder/header no longer cause errors.

Improved C frontend

• The C frontend now supports:
  • uses of the keyword _Generic in initializers for objects of static storage duration
  • _Alignof(void) as a C language extension, supported by various compilers; the result of this expression is 1
  • the __attribute__((weak)) for weak linkage of identifiers
  • wide string literals and UTF-8 string literals
  • more cases of universal character names in strings
  • using the $ character as part of identifiers (C language extension)
  • universal character names as content of character constants and string literals
  • compound literals of array type without explicit size
  • applying sizeof to unions that contain structs with flexible array members
• Tags declared in the parameter declaration list of a function definition are now made visible in the function body.
• Support for expressions with the conditional operator (a ? b : c) where b is a pointer and c the null pointer constant (void*)0.
• Non-standard escape sequences are now accepted and reported. They are replaced by the character after the backslash.
• asm is now considered to be a keyword, and is handled like __asm.
• Bit-fields of enum type are now longer rejected if not all elements of the enum are within the range of the resulting bit-field.
• The signedness of a bit-field of enum type now always has the same signedness as the respective enum type. In previous releases, the signendess of such bit-fields was determined by the ABI option bitfield_sign. The new behavior corresponds to the behavior of common compilers, like GCC and Clang. Please also see release notes for the new diagnostic rule A.3.3.
• The following types are no longer considered compatible:
  • Different struct/union types from the same translation unit.
  • Different floating types of equal size.

Other frontend improvements

• Improved dependency cycle detection for the abstract domain of arithmetic-geometric progressions (dev-geo). Dependency cycles are now detected through more cases of function pointer calls, thus increasing the precision of the analysis in cases like the following:

  void g(void);
  typedef void (*fptr)(void);
   
  void main(void)
  {
    fptr f;
    while(1) {
      f = g;
      (*f)(); /* dev-geo can now improve precision on code called through f */
    }
  }

• The analyzer now accepts undefined objects of static storage duration with incomplete type that are not referenced in the code.
• Modified the evaluation of function calls to ensure that parameters are always evaluated in left to right order, as documented in the user manual. Please note that this order is unspecified by the C norm. Code that relies on a particular evaluation order violates the diagnostic rule A.4.1, as well as the coding rules CERT.EXP.30, M.12.2, and M2012.13.2.

ABI

When evaluating initializers for objects with static storage duration, Astrée now uses the ABI option rounding_mode_for_constants instead of rounding_mode.

Options

• The gauge domain is now active by default (gauges=yes).
• New option warn-on-signed-integer-lshift-ranges enables alarms about left shifts of negative values. The option is disabled by default.
• The option log-iter now takes an integer value that specifies after how many up iterations the analyzer starts logging the fixed-point iteration of a loop. The default value is 10, and the value -1 disables logging.
• Improved the heuristic for context-insensitive analysis (triggered by the option separate-analysis=*) in case of multiple asynchronous processes. The heuristic now computes a different set of “separate functions” for each process, which generally improves analyzer performance.
• The option automatic-partition no longer partitions division operations.

Command-line options

• The options --report-file and --xml-report-file file are no longer restricted to batch mode execution. They are now also accepted in GUI mode.
• The deprecated batch mode options -u and --files <files> have now been removed.

Directives

• Fixed an analyzer crash that could happen when using an __ASTREE_partition_begin directive on a variable with too many possible values.
• The tool now supports external comments for RuleChecker alarms in original source files. To this end, the new source level directive RULECHECKER_comment allows commenting rule violations at arbitrary code locations. The GUI automatically generates AAL annotations with such directives when commenting alarms in the Findings view. Thus, users can now comment all findings of the tool directly from the Findings view.
• AAL annotations now support identifier substitutions per annotation block. These substitutions are applied to the text of the directives before inserting them in the code. For example, the annotation block

  __ASTREE_annotation((
    OTHER=STRANGE;
    STRANGE=THING;
    ANY=x;
    SOME=y;
    THING=b;
    main { -1 statement} insert before : __ASTREE_log_vars((ANY.OTHER)); 
    main { -1 statement} insert before : __ASTREE_log_vars((SOME.THING));
  ));

  generates the following directives:

  __ASTREE_log_vars((x.b);
  __ASTREE_log_vars((y.b);

• Harmonized the error handling of modify and initialize directives. The directives

  __ASTREE_initialize((expr));
  __ASTREE_modify((expr; initialize));
  __ASTREE_modify((expr; full_range));

  now behave exactly like

  __ASTREE_modify((expr));
  __ASTREE_modify((expr; [lo, hi]));

  in case that the evaluation of expr has no valid result. The analyzer raises an error and continues the analysis ignoring the invalid effects of the directive.
• Improvements and clarifications for the __ASTREE_global_assert directive:
  • When a global assertion fails, Astrée now outputs the name of the variable concerned with the failed assertion. This is particularly useful when global assertions are violated by indirect write accesses through pointers.
  • If a variable appears at the same time in an __ASTREE_global_assert and in an __ASTREE_smash_variables directive, the analyzer now ignores one of the directives and reports a violation of the diagnostic rule A.5.1. Moreover, it now prevents dynamic smashing of globally asserted variables.
  • In addition to direct assignments, __ASTREE_global_assert now also keeps track of modifications via byte-level directives, such as __ASTREE_bzero or __ASTREE_trash, and type punning. The analyzer will now also raise an alarm if a globally asserted variable is modified through a call to __ASTREE_modify.
  • The directive no longer cuts execution traces when analyzing a weak assignment in which the assertion does not definitely fail on all targets of the assignment.
  • __ASTREE_global_assert now also enforces the asserted bounds if the bounded variable is affected by a data race.

Alarms, messages and warnings

• The analyzer now explicitly warns about too large variable arguments (unsupported language feature) by raising an invalid call alarm. Execution traces with such alarms are discarded (analyzer raises an error).
• Clicking on preprocessor and C++ parse errors now opens the editor view to display the corresponding code.
• In addition to the "Definite run-time error" messages that can follow class A alarms, the analyzer may now also raise error messages if the analysis stops in some context for other reasons, such as immediately preceding errors or contradictions in the information computed by the abstract domains.
• The analyzer no longer rejects code with double defined functions. Instead it raises an error and continues with the analysis, using one of the two function definitions.
• The analyzer no longer issues false alarms about possible non-termination of loops that are only left via goto.
• Using the deprecated syntax [lo-hi] for array slices (e.g. in __ASTREE_modify) now triggers an error instead of just a notification. These errors can be removed by rewriting such expressions using the new [lo..hi] syntax.

Improved reporting

• Improved the output of iteration phases and iterations in the analyzer log and added time stamps to track analysis progress and current memory consumption. This is especially useful for observing the progress of long-running Astrée analyses.
• Improved error reporting of the C frontend when the code contains invalid Astrée directives.
• Improved error reporting for __ASTREE_alarm, __ASTREE_comment, and __ASTREE_suppress directives if the specified alarm type is invalid.
• Improved the output of the log-time option in the analyzer log and text report file. The timing statistics for each function are now printed in the same tabular form that is used for reporting reachable/unreachable/stubbed functions.

Server and server controller

• Fixed an issue that could cause the server controller to lose server connections in high-latency networks.
• Fixed an issue with the server becoming unresponsive when a client uses “Display invariants” or the Watch view in large analysis projects.
• Fixed an issue that could leave nameless projects on the server, depending on its configuration and state. It occurred mostly during QSK runs.
• Improved the handling of ALM licenses.

Client and GUI

• When suggesting comment directives for rule violations, the GUI now considers the full extent of the alarm location. Pasting the suggested directive into the code should therefore now work in all circumstances. In previous releases, the second argument of the suggested directive (the number of lines) needed to be modified if the alarm extended over more than one line of code.
• Improved syntax highlighting for C, C++, and the AbsInt annotation languages.
• The Annotations view now provides a context menu entry for exporting a single block of annotations into an AAL file.
• AAL files are now exported using UTF-8 encoding instead of using the locally preferred encoding.
• Improved detection and prevention of recursive DAX imports.
• Improved the expansion of environment variables in DAX files to allow the use of more than one environment variable in an XML text node or attribute value.
• Custom report configurations can now filter the list of findings by their alarm classification (undecided, true, false, etc.) as specified by the user. This feature is equivalent to filtering the findings by their classification in the Findings view of the GUI.
• Added the keyboard shortcut Ctrl+I to editor views for preprocessed code for inserting an annotation at the current cursor position.
• The XML report and the custom report files now contain all rule configurations together with their list of active rules.
• Value tooltips for expressions spanning multiple lines are now displayed correctly in the GUI.
• Fixed the control-flow overview in case of analyses with control-flow insensitive analysis of some functions (option separate-function). It now displays all caller/callee relationships.
• Fixed an issue in the Findings view that could cause the comment text to be reset while editing.
• Fixed an issue in the report file generation that could lead to text report files without analysis result summary.
• Fixed the message category filtering for custom reports.
• Fixed the display of analysis duration in case that the server and client run on computers with different time settings.

MISRA C++:2008

• Added support for 33 more rules:

  • M2008.0.1.2, M2008.0.1.4
  • M2008.2.10.1, M2008.2.10.3, M2008.2.10.4
  • M2008.3.2.1, M2008.3.2.2, M2008.3.2.3, M2008.3.2.4
  • M2008.3.9.1
  • M2008.5.0.1
  • M2008.6.5.4, M2008.6.5.5, M2008.6.5.6, M2008.6.6.3
  • M2008.7.3.1, M2008.7.3.5, M2008.7.5.1, M2008.7.5.3, M2008.7.5.4
  • M2008.8.5.1, M2008.8.5.2
  • M2008.9.3.1, M2008.9.3.2
  • M2008.10.2.1, M2008.10.3.1
  • M2008.15.3.6, M2008.15.4.1
  • M2008.16.0.2, M2008.16.0.8, M2008.16.2.2, M2008.16.6.1
  • M2008.17.0.2
• Fixed the check array-argument-to-pointer-decay for rule M2008.5.2.12. It failed to warn about arguments decaying to pointers if the corresponding parameters of the called function were declared const.
• The check integral-type-name (rule M2008.3.9.2) no longer warns about bit-fields.

MISRA-C:2004 and MISRA-C:2012

• Extented coverage of the rules M2012.D.4.11 and M.20.3.
• New checks:
  • non-standard-identifier (M.1.1 and M2012.1.2) warns about the declaration/definition of identifiers that contain a $ character.
  • undeclared-parameter, introduced for the new diagnostic rule A.1.10, is now also associated with the rules M.1.1, M.8.2, M2012.1.1, and M2012.8.1.
  • The rules A.2.14 and A.2.15 now warn about uses of the newly supported language extensions #include_next, __has_include(), and __has_include_next(). Checks for the rules M.1.1 and M2012.1.2 have been extended accordingly.
• Improved checks:
  • The checks evaluation-order and evaluation-order-initializer no longer produce false alarms for array look-ups in which the index expression is a function call, as in a[f()]. This affects rule M.12.2 and M2012.13.2.
  • Fixed the “essential type” assumed for arithmetic operators with operands that are const-qualified lvalues, in order to remove false alarms for rule M2012.10.6.
  • Improved the precision of the check return-implicit to remove false alarms for rule M.16.8 and M2012.17.4.
  • The checks controlling-invariant (rule M2012.14.3) and boolean-invariant (rule M.13.7) now also warn about invariant expressions when there is control flow by break, continue or goto circumventing the expression.
  • The check integral-type-name (rule M.6.3 and M2012.D.4.6) no longer warns about bit-fields.
  • The rule check external-redeclaration for rule M2012.8.5 no longer warns about declarations if only their column offsets in preprocessed code differ.
  • The check expression-statement-dead (rule M2012.2.2) now also warns if the increment part of a for-loop is dead.
  • Rule M.1.1 and M2012.1.2 now warn about sizeof or _Alignof applied to void.
  • The check essential-arithmetic-conversion (rule M2012.10.4) is no longer triggered by a ternary operator with a null pointer constant as second or third operand and a pointer as the other operand.
  • The check parameter-missing-const no longer causes false alarms for rule M.16.7 and M2012.8.13.
• Improved reporting of:
  • source location for the rule check pointered-deallocation
  • violations of rules M12.5.* and M.5.*, where both conflicting code locations are now reported

SEI CERT Secure C

• Added support for 28 more rules:

  • CERT.ARR.30
  • CERT.CON.37, CERT.CON.40
  • CERT.DCL.40
  • CERT.ENV.30, CERT.ENV.33
  • CERT.ERR.30, CERT.ERR.33
  • CERT.EXP.33, CERT.EXP.36, CERT.EXP.37, CERT.EXP.40, CERT.EXP.42, CERT.EXP.44, CERT.EXP.45
  • CERT.FIO.41
  • CERT.FLP.37
  • CERT.MEM.33, CERT.MEM.35
  • CERT.MSC.30, CERT.MSC.40
  • CERT.SIG.30, CERT.SIG.31, CERT.SIG.34
  • CERT.STR.30, CERT.STR.34, CERT.STR.37, CERT.STR.38
• The checks evaluation-order and evaluation-order-initializer no longer produce false alarms for array look-ups in which the index expression is a function call, as in a[f()]. This affects rule CERT.EXP.10 and CERT.EXP.30.
• Improved the precision of the check return-implicit to remove false alarms for rule CERT.MSC.37.
• The check undeclared-parameter, introduced for the new diagnostic rule A.1.10, is now also associated with the rule CERT.DCL.31.
• Improved the check parameter-missing-const to remove false alarms about violations of rule CERT.DCL.0 and CERT.DCL.13.

MITRE CWE

• The check expression-statement-dead (rule CWE.561) now also warns if the increment part of a for-loop is dead.

Diagnostics

• New diagnostic rules:
  • A.1.10 warns about undeclared parameter identifiers in function definitions with identifier-list, for example:

    int f(v) { return 0; } /* parameter v is not declared */

  • The new rule check non-standard-identifier (rule A.2.12) warns about the declaration/definition of identifiers that contain a $ character.
  • A.2.13 warns about sizeof or _Alignof applied to void.
  • A.2.16 warns about the use of __attribute__, in particular to notify about __attribute(weak), which is a newly supported language extension.
  • A.3.3 warns about implementation-defined bit-field types.
  • A.5.3 (check unsupported-language-feature-fatal) warns about the use of language features that are not supported by Astrée and may cause the analyzer to terminate with an error.
• Rule A.5.1 now also warns about invalid Astrée directives that are inserted via AAL annotations.
• The rules A.2.14 and A.2.15 now warn about uses of the newly supported language extensions #include_next, __has_include(), and __has_include_next(). Checks for the rules M.1.1 and M2012.1.2 have been extended accordingly.
• The checks evaluation-order and evaluation-order-initializer no longer produce false alarms for array look-ups in which the index expression is a function call, as in a[f()]. This affects rule A.4.1 and A.4.2.

Style and naming rules

• Style checking of function pointer names now takes the option type-abbreviations into account.
• Naming rule checks now support the placeholders %plaintype%, %Plaintype% and %PLAINTYPE% which represent the type abbreviation of the named object without recursive expansion by pointee type (in contrast to %Type%).

Customer-specific rules

• The rule checks integral-type-name and integral-type-name-extended for rule X.A.5.6 no longer warn about bit-fields.

Other changes

• Rule sets are now folded by default for a better overview in the Rules Configuration view.
• Write accesses to multi-dimensional arrays no longer trigger the check uninitialized-local-read.
• Several checks have been split as follows:

  pointer-qualifier-cast	↗ ↘	pointer-qualifier-cast-const pointer-qualifier-cast-volatile
  pointer-qualifier-cast-implicit	↗ ↘	pointer-qualifier-cast-const-implicit pointer-qualifier-cast-volatile-implicit
  directive-syntax	↗ → ↘	directive-syntax extra-tokens non-directive

• Fixed a crash triggered by the rule checks recursion and uninitialized-local-read.

Stub libraries

• The osek.h header file of the OSEK stub library can now be extended by defining the macro _OSEK_H_PRE_INCLUDE in pre­processor configurations:

  <defines>
    <define>_OSEK_H_PRE_INCLUDE="${A3_GLOBAL_BASE_DIR}/my_osek_vendor_extensions.h"</define>
  </defines>

• The OSEK stubs now declare event masks in a way that allows their use in constant expressions. This change fixes compatibility issues that could prevent the analysis of OSEK applications with earlier versions of Astrée.
• The C stub library now provides more precise implementations for strcmp and strncmp and checks argument pointers that are not explicitly used otherwise. In case of such a pointer being NULL or invalid, the analyzer raises an alarm at the program point where the stub is invoked.
• The C stub library constants UINT_MAX, ULONG_MAX, and ULLONG_MAX are now defined as unsigned.

Compiler configurations

Added support for new built-in functions of CompCert for 32/64-bit hybrid PowerPC introduced in CompCert release 18.10.

Preprocessor

• The new environment variables $A3_GLOBAL_BASE_DIR and $A3_BASE_DIR can be used in preprocessor configurations to refer to the global base directory of the analysis, or the base directory of a preprocessor configuration, respectively.
• Fixed issues with RuleChecker projects containing C preprocessor configurations that inherit defines and includes from C++ preprocessing configurations.

Slicing

The built-in program slicer now supports context sensitive slicing for tasks of concurrent programs.

Integration with TargetLink

• Added support for TargetLink 4.3.
• The AbsInt Toolbox for TargetLink no longer sets the cleancode option when generating code for Astrée analyses. This modification prevents issues when using the Toolbox in cases where the cleancode option is read-only.
• To invoke RuleChecker from Matlab, AbsIntManager now provides a new method InvokeRuleChecker(). The second argument to InvokeAstree() which was previously used to choose between Astrée and RuleChecker is now deprecated.

Other changes

• Incremented the DAX version number to 1.5. DAX files of previous versions can still be imported.
• The Windows executable installer supports a new command line option /datadir='dir' for configuring the server data directory.
• In the analysis log and text report files, the project information that used to be a single long line is now broken up into several lines:

  *** Project name: Scenarios
  *** Description: Standard example
  *** Id: 1016452227
  *** Revision: 1

• Descriptions may now contain line breaks.

Qualification Support Kits

• Improved performance of QSK execution.
• 3 new test cases for Astrée:
  • qk_aal_identifier_substitution
  • qk_alarm_negative_lshift_argument
  • qk_option_warn_on_signed_integer_lshift_ranges
• 22 new test cases for RuleChecker:
  • qk_check_non_standard_escape_sequence
  • qk_check_non_standard_identifier
  • qk_check_undeclared_parameter
  • qk_check_attribute
  • qk_rule_a_2_11, qk_rule_a_2_12, qk_rule_a_2_13, qk_rule_a_2_14, qk_rule_a_2_15, qk_rule_a_2_16, qk_rule_a_3_3, qk_rule_a_5_3
  • qk_check_recursion
  • qk_check_stdlib_limits
  • qk_check_alignof_void, qk_check_sizeof_void
  • qk_check_has_include, qk_check_has_include_next, qk_check_include_next
  • qk_aal_insert_source_comment
  • qk_directive_comment_source_external
  • qk_check_unsupported_language_feature_fatal

Bug fixes

• Fixed an issue that could cause the analyzer to stop with an error message when casting negative intervals into smaller types.