Astrée release 15.04

General

  • The C stub library now supports 16-bit and 32-bit architectures. The correct configuration is inferred from the size of a pointer in the ABI settings.
  • When opening for the first time an analysis created with an older release, verify your local set­tings (Preprocessing, Reports, Code generators). In rare cases, the automatic conversion may produce invalid entries.

Precision

  • The analyzer now computes significantly more precise intervals for expressions using the bitwise operators AND (&), OR (|), and XOR (^).
  • The new option partition-pt1 partitions first order lag (PT1) elements of the form x + (i - x) * c to allow for a more precise analysis. This option is enabled by default.
  • The new non-relational domain of congruence intervals adds precision when dealing with deeply nested structures and arrays. It is activated via the new option congruence-intervals=yes.
  • With the new option exclude-signed-in-unsigned-overflows=yes, Astrée keeps precise information for signed values that are explicitly cast to unsigned. When casting the unsigned result back to signed, the analysis can then yield a more precise result. The analyzer reports overflows of signed values in unsigned computations only if the overflow also occurs in the signed representation. This feature is particularly useful for analyzing TargetLink-generated code. In addition, the new option exclude-signed-negation-overflows-in-cto=yes will exclude alarms raised by signed negations (when negating the smallest representable integer of a given type) when that negation occurs after casting an unsigned with CTO semantics.

C language features

  • Added support for compound literals like &((struct s){0}).
  • Astrée now accepts non-standard empty initializer lists (e.g. int arr[] = {};) which are supported by many C compilers.
  • Added support for the keyword typeof (GCC extension). Astrée can now analyze code such as int x = 3; typeof(x) y = 900 / x;
  • The new option anonymous-global-structs-and-unions=yes enables support for global anonymous structs and unions. This is a C language extension supported by some compilers. Astrée implements the behavior of the IAR compiler and names such objects after their first field with the prefix _A_.
  • The analyzer now accepts functions with variable argument lists.

Directives

  • New:
    • __ASTREE_trash for use in stub functions (e.g. the C library stubs). It models a random modification of a given number of bytes of memory starting from a given address.
    • __ASTREE_access((var, size)); models a read access on the first size bytes of the variable var.
    • __ASTREE_huge_valf() and __ASTREE_huge_val() return positive infinity as a floating constant of type float or double, respectively. They are used to implement the standard macros HUGE_VAL, HUGE_VALF, and INFINITY in the C stub library.
    • __ASTREE_va_start((param)); allows implementing the va_start macro of the C standard library for initializing a va_list object to handle variable argument lists. An implementation of the macro (together with corresponding declarations of the va_arg, va_copy, and va_end macros) can be found in the standard C library stubs that are installed with Astrée.
    • __ASTREE_malloc can be used to implement malloc, realloc, and free. Stubs for these functions have been added to the Astrée C library to illustrate the usage of the new directive.
  • Improved and extended:
    • The __ASTREE_comment directive now accepts new types of comments for alarms. In addition to false, true or undecided, an alarm message can now also be classified as true_high, true_low or true_no_defect.
    • The directive __ASTREE_absolute_address has been extended to also work for static variables.
    • The analyzer now accepts __ASTREE_partition_control directives before for-loops with declarations, e.g. 
      __ASTREE_partition_control((12)) for (int i = 0; i < 12; i++)
    • It is now possible to keep the partitions created during a function call after the return point. To that end, the function call should be preceded by the directive __ASTREE_partition_control (such as in __ASTREE_partition_control f(4);).
    • Generalized the __ASTREE_modify directive to allow modifying lists of values and specifying new ranges for modified values. For example, the annotation 
      __ASTREE_modify(( x, y[0-3], z->p; [11,42] ));
      sets the value range of x, y[0], y[1], y[2], y[3], and z->p to the interval [11,42].
      Note that this extended directive can raise a new kind of alarm if the specified interval is invalid.

Options

  • The new option ais-export=yes enables the collection of information about calls via function pointers. The collected information can be exported into an AIS file for use by a³ binary-level static analyzers (e.g. StackAnalyzer).
  • Removed the option show-hints.
  • Removed the option stop-parse-error-delayed which allowed starting the run-time error analysis even if there were parse errors in the preprocessed files. All preprocessed files in the project must now either be accepted by the analyzer or removed.
  • Added a new option list-entry-functions=n for collecting all functions with the maximum call depth of n. The collected information is used to display a list of potential entry functions for the analysis.
  • The option separate-function is now fully compatible with the data flow options dump-dataflow and report-shared-variables.
  • There are two new ABI settings, rounding_mode and rounding_mode_for_constants. The latter is used for the parsing of constants and the former is used for all other floating-point operations. Both options can be set to to_nearest or to all. The latter means that no assumption is made by the analyzer concerning the rounding mode. The default rounding mode for constants is to_nearest (as required by the C standard), while for the other operations it is all. For architectures using internal representations with more than 64 bits for doubles, rounding_mode should always be set to all since the double rounding is not equivalent to rounding to nearest.
  • Replaced the option warn-on-initializer-ranges=yes by the new option exclude-overflows-in-initializers=no.
  • Removed the option honor-cto-comments for suppressing alarms in expressions marked with TargetLink’s CTO comments. It is no longer needed since the analyzer can now auto­matically exclude the undesired alarms by semantics-based reasoning activated via the new option exclude-signed-in-unsigned-overflows.

Fixes

  • Fixed the clock domain which could cause very high analysis times in release 14.10 and release 14.10i with build numbers below 234645.
  • Fixed analyzer crashes when dealing with variables allocated to the absolute address 0.

MISRA-C:2004

  • Added support for rules 3.4, 5.7, 12.1, 12.6, 16.7, 19.3, 19.7, 19.9, and 21.1.
  • Extended support for rule 16.8.
  • Fixed check missing-else for rule 14.10 of MISRA 2004. The Rule Checker no longer warns about single if statements without else. MISRA requires a final else clause only for if ... else if ... cascades.
  • The checks rule 5.4 have been refined and now also take enum tags into account.
  • Fixed check for rule 8.12. The respective rule check is no longer restricted to header files.
  • Improved the precision of MISRA-C rule checking to remove false alarms for the checks include-syntax, plain-char-usage, and statement-sideeffect.
  • Fixed false alarms concerning violations of rule M.8.8 and M.10.1.
  • Extended the checks for rule 20.2 to declared identifiers.

MISRA-C:2012

Added support for the MISRA-C:2012 rule set.

Other

  • Added a second comment density code metric that follows the HIS definition.
  • The Rule Checker can now also check naming conventions for variables, functions, macros, and user-defined types. Valid names can be specified via regular expressions. The feature is found in the new “Style rules” category in the options.
  • The Qualification Support Kit package that validates the Rule Checker is no longer an add-on to the basic Astrée QSK that validates the run-time error analysis. The two QSKs are now separate and require separate qualification test runs.

New features

  • All-new Result Viewer for exploring all findings of the analyzer. It displays a list of alarms and errors which can be easily browsed, sorted, and filtered. A single click on a finding loads all relevant information, such as the source code with tooltips and the list of all relevant contexts. Each finding can be classified and commented by the reviewer. Available classifications are:
    • true error
    • true error with high priority
    • true error with low priority
    • true error that is not considered a defect in the software under analysis
    • false alarm
    • undecided
    The results of the review appear in the XML reports and summaries. It is not necessary to re-run the analysis.
  • It is now possible to generate AAL annotations automatically by simply right-clicking into the code displayed in the editor and selecting “Generate Annotation” from the context menu. After specifying a directive to insert, Astrée automatically generates the AAL specification that places the directive at the selected position in the code. The analyzed code is not modified.
  • Added a new display of potential entry functions (periodic tasks and initialization functions) based on a pre-analysis of the source code. The list is available via the Tools menu, and is also displayed automatically if no analysis entry point was specified. Relevant tasks and initialization functions can then be selected to configure the analysis. Collecting information about potential entry functions can be disabled via the new option "list-entry-functions".
  • The new editor view mode preference (accessible via Project → Preferences → Editor) allows to change the default view for preprocessed code. Available choices are Original source, Preprocessed source, and Split view which displays the original and preprocessed sources side by side.
  • The Preferences dialog has been extended by a field for specifying a user name for authentication with the Astrée server.

Improvements

  • Improved editor layout and performance when adding a large number of annotations to the exact same program point.
  • In the Output view of the GUI, it is now possible to copy not only whole lines but also line parts.
  • The extraction of AAL annotations from the source files can now be canceled using either the stop button in the menu bar or the "Stop extraction" button in the "Advanced" tab of the Annotations view.
  • Importing an Astrée options file (via Project → Import → Options) now only affects options that are listed in the imported file. Other options are no longer reset to their default value.
  • The "new project" wizard can now be skipped (added finish button).
  • It is now possible to jump directly back to the last displayed editor view by clicking on the "Files" entry in the project side bar or pressing Alt + E.
  • Modified the default behavior when loading a DAX specification that references a wrapper file and at the same time contains further tags in the <wrapper> section. In this case, Astrée no longer re-generates the wrapper automatically but uses the referenced .cfg file. Running a batch mode analysis with such a file behaves likewise.

Fixes

Fixed the actions “Select category”, “Unselect category”, “Select all”, “Unselect all” in the context menu of the Rules options. This fixes a known issue from release 14.10.

Toolbox and Data Dictionary import

  • Astrée now imports value range annotations from the Data Dictionary also for calibration variables of vector and matrix types, and for variables with the flag volatile=off.
  • Fixed an issue that prevented the usage of the AbsInt Toolbox with MATLAB versions older than 2013a (removed the usage of strsplit).
  • Improved the detection of available subsystems in the Toolbox. This fixes issues with missing stub functions for lookup and interpolation routines.
  • Optimized annotations generated for TargetLink’s linear search interpolations.
  • Added an option to the AbsInt Toolbox for running a user-defined MATLAB script, e.g. for generating additional AAL annotations, before starting the Astrée analysis.
  • The DD import now also annotates ranges for array parameters.
  • The DD import now also generates assertions for vector outputs.
  • Bounds for scaled fixed point values are now always rounded to integer numbers. Rounding is downwards for lower bounds and upwards for upper bounds.
  • Added a new option for adding the source files of the DSFxp library to an analysis.
  • Improved generated directives for RTE-Frame variables.

Server

  • The server data directory name may now contain special characters (like é).
  • The server now closes all open client connections when the data directory is changed via the server controller.

Documentation

The Astrée documentation has been extended by a new manual containing detailed compliance matrices for Astrée regarding undefined/unspecified/implementation-defined behaviors according to the C99 standard.