Astrée release 14.10

MISRA rule checker

Astrée is now able to check coding rules (MISRA), compute code metrics (comment density, cyclomatic complexity, etc.), and check metric thresholds. The rule checker is highly configurable, allowing users to toggle checks for individual rules or aspects of certain rules.

The majority of the checks is performed syntactically, either on the source code or on the preprocessed code. It is possible to skip the runtime error analysis and only perform the rule checks.

A few more checks, for which a purely syntactic analysis would be too imprecise, are performed during the runtime error analysis. If a selected coding rule is violated, the analyzer reports an alarm of the new category R and reports the violated rule together with the exact code location and the check which failed.

New options and preferences

  • The editor view of the GUI now displays directives like __ASTREE_unroll or __ASTREE_partition_control which have been inserted automatically by the analyzer. Displaying such automatically inserted directives can be turned off and on in the Preferences dialog.
  • The batch mode of Astrée now accepts a new parameter --stop for stopping an analysis that is running on the server.
  • The analyzer can now be configured to not stop upon the first parse error (stop-parse-error-immediate=no) but to continue and optionally stop before starting the actual analysis (stop-parse-error-delayed=yes). Files with parse errors are discarded after reporting the error.
  • The smallest addressable unit of the target platform can now be configured using the new ABI option bits_of_byte. It accepts the values 8 and 16, the default being 8. When the value 16 is used, the additional option bits_of_char configures computations on values of type char to have either 8- or 16-bit precision.
  • The administrative connection to the Astrée server via the server controller can now be protected by an administrator password.
  • Analysis projects can now be flagged as private by the project owner to hide them from other users.
  • Removed options:
    • verbose-variable-alarm, as alarm messages of the analyzer are now always verbose.
    • warn-in-simplify, as all run-time errors that can be found during constant propagation and simplification are also reported by the subsequent run-time error analysis.

AbsInt Toolbox for TargetLink

  • The toolbox can now be installed into either $TLROOT/matlab/local or $MLROOT/toolbox/local.
  • Improved collection of relevant files for the analysis of projects that use incremental code generation.

Qualification Support Kits

Added new QSK test cases for validating the “External Declarations” feature.

Known issue

The server data directory’s name must not contain special characters, including accented letters or umlauts.

  • The order of application for parser filter patterns has been modified. The analyzer now first applies all function patterns in the order in which they have been specified. It then applies all identifier and regular expression patterns, again in the order in which they have been specified.
  • The result summary in the analyzer output now contains information about the number of reached program statements, e.g. 
    /* Result summary */
Reached 26 of 26 statements during the analysis.
  • Improved the precision of the analyzer when analyzing function calls with parameters of the form (cond ? expr1 : expr2).
  • Improved the identifier search feature when searching for uses of a variable in the analysis project. It is now possible to distinguish between accesses that read, write, or take the address of a variable.
  • Generated analysis wrappers now always consider that tasks from the main loop may be called in an arbitrary order, even if the functions have different signatures and therefore cannot be called via a single function pointer table.
  • Fixed suppression of overflow alarms for suppress directives with type conversion_overflow or arithmetic_overflow.
  • The default value for unrolling outer loops has been reduced to 1. The new default is better suited for the most common type of analyses in which all tasks are called from an infinite main loop. In this case, more unrolling of the main loop often does not yield better results but only increases the analysis time.
  • Uses of the following directives are now reported in the “further directives” section:
    • _ASTREE_smash_variable((local_variable))
    • _ASTREE_double_exp_2
    • _ASTREE_double_sqrt
    • _ASTREE_import
  • Improved the precision for conditional statements that involve comparisons of expressions with explicit casts.
  • It is now possible to add multiple (leaf) revisions of the same analysis project to the analysis queue of the server.
  • Fixed occasional crashes of the GUI when uploading a large number of files at once to the server.
  • Fixed parsing of line directives of the form “#line 123” which could fail when using parser filters.
  • When the automatic stubbing is activated, Astrée no longer warns when the stubs are created, but only when they are called.
  • Improved coverage computation which sometimes erred on the lower side (actual coverage was higher than reported).
  • The analyzer now also supports casts between function and data pointers (common extension J.5.7 of ISO/IEC 9899:1999).
  • Improved precision for modulo operations in loops.
  • Messages in the <messages> section of the XML report now feature the actual message text as one or several <textline> tags.
  • Fixed issues with very long path names on Windows.
  • Fixed the implementation of the <id> tag in DAX files. It now behaves exactly as documented.
  • The XML alarms-per-file summary file and the XML report file are now generated when running a batch mode analysis with a DAX file that specifies these files in its <reports> section.