Astrée Release 14.10

New 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 and it is possible
to skip the run-time 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 run-time 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.

Other improvements
* 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.

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

Last modified on 1 October 2014 by
Copyright 2014 AbsInt.
An HTML version of these release notes is available at