Astrée and RuleChecker Release 18.10

Eclipse plugin
An Eclipse plugin for Astrée and RuleChecker is now available. 
The plugin is also part of 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. See also the 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 manual. 
  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.

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

▲ 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, 
  but are also accepted in GUI mode.
▲ The deprecated batch mode options -u and --files <files> 
  have now been removed.

▲ 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

      main { -1 statement} insert before : __ASTREE_log_vars((ANY.OTHER)); 
      main { -1 statement} insert before : __ASTREE_log_vars((SOME.THING));
  generates the following directives:

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

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

  now behave exactly like

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

▲ 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.FIO.41
  △ CERT.FLP.37
  △ CERT.MEM.33, CERT.MEM.35
  △ CERT.MSC.30, CERT.MSC.40

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

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

▲ 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 to RuleChecker --------------- ▲ 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 preprocessor 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.