Astrée release 13.04

General

  • Improved precision when handling strict float comparisons (!=, <, >) in octagons.
  • Synthetic (internal) variables are now automatically inserted into octagon packs.
  • Trace partitions created in a function call can now survive the function return if the call is preceded by __ASTREE_partition_control.
  • Context descriptions (e.g. in alarm messages) now also contain loops that are not unrolled. Such loops appear as loop@XXX>=1.
  • Implemented the evaluation of constant conditional expressions (e.g. const int i8 = 0 ? -1 : 7) when running the analyzer with constant folding disabled (simplify=no).
  • Improved the use of octagon constraints when reporting potential runtime errors. This allows the analyzer to automatically remove alarms for code such as if (a - b > 0) { d = c / (a - b); }
  • Improved location information in some alarms to precisely refer to a certain operand in a comparison or arithmetic expression.
  • Improved the precision of modulo computations with pointers such that the result of evaluating expressions like ((unsigned int) ptr % 4) is in the expected positive range ([0,3] in this example).
  • The precision of notifications about potential ambiguities due to side effects in expressions has been improved, so that the analyzer now reports fewer false positives. The corresponding message has been renamed from “Potential side effects in expression” into “Potential ambiguity due to side effects in expression”.
  • A new category of alarms, ALARM(D), has been added to represent messages about uninitialized variables. As messages of this kind do not represent run-time errors, they do not influence the behavior of the traffic lights. As long as there are no errors and only alarms of class D, the traffic lights remain green.
  • The identifiers “asm” and “packed” are no longer treated as keywords.
  • The analyzer now allows the construction of pointers to undefined functions. Such pointers are then invalid.

Options

  • The analyzer now warns about incompatible combinations of options.
  • New options:
    • fold-contiguous-fields
      allows to treat sets of contiguous structure fields of the same type as arrays for the purpose of smashing.
    • warn-on-undefined-remainder
      enables warnings when computing (signed INT_MIN % (-1)) which is undefined according to the 2011 revision of the C norm.
    • export-fold
      controls whether all contexts should be joined before exporting invariants in order to reduce memory consumption, thus enabling the use of tool tips and the watch window for much larger projects.
    • dump-dataflow
      allows to specify whether data flow information should be collected during the analysis run.
    • fields-in-octagon-packs=yes
      allows adding structure fields to octagon packs.
    • interproc-oct-packs
      allows interprocedural octagon packs.

Directives

  • The __ASTREE_absolute_address directive now accepts absolute address specifications with standard suffixes like 0xfffff0000u.
  • Added new directive __ASTREE_check which behaves like __ASTREE_assert, except that it doesn't restrict the ranges of checked variables.
  • The __ASTREE_partition_begin directive has been optimized for enum types. Instead of partitioning all possible integer values, it partitions the possible enum values and the ranges between them. Thus, partitioning according to variables of enum type becomes feasible even if the analyzer must assume a large number of potential values for these variables.
  • Fixed the order in which AAL annotations from different annotation blocks are inserted.

GUI

  • A single click on a file in the Project tree opens it only if the file has already been downloaded from the server. Downloading a file from the server is triggered by a double click.
  • The result views now use the system default for mouse clicks. On most systems items now react on double click.
  • Inline assembly statements which are not filtered but automatically ignored by the analyzer, e.g. __asm("addl $4, %esp"); are now also marked in the GUI as being filtered.
  • The watch feature has been generalized to display not only plain variables but also more general lvalue expressions, e.g. *var, var.field, var->field, var[N], etc.
  • The original source view can now display HTML formatted source files generated by TargetLink or Embedded Coder. Thus it becomes possible to jump from the original source code view in Astrée directly into the Matlab model.
  • The editor tab size can now be configured in the preferences dialog.
  • When synchronizing files between the local machine and the server, error messages of the GUI now state which local files are missing and which local files are identical to the server files.
  • The Preprocessing view now accepts defines that include whitespace characters (e.g. UINT=unsigned int).
  • When setting up a new project, the list of files to analyze can now be given as a text file. Each file must appear on a separate line.

Server

  • Improved client–server communication to prevent unexpected connection aborts.
  • The server now takes additional precautions to avoid damaging its configuration files when the hard drive is full.
  • User-specific information is now attached to a certain Astrée installation instead of a host name. Hence, the local settings of users are now preserved even if the host name changes.

Qualification Support Kits

Fixed misspellings and inconsistencies in the VTP and TOR documents and the test reports.

Other improvements

  • All defines in the example C stub library are now guarded to prevent collisions when preprocessing source code which sets standard defines before including standard headers.
  • When running an analysis in batch mode with the option -u, the execution now stops with an error code (an exit code that is not equal to 0) if some local files are missing. In addition, a detailed description of the error is printed into the report file (specified via the option --report-file).

Bug fixes

  • Fixed assertion failures when activating dynamic smashing and uninitialized warnings.
  • Fixed Boolean packing heuristic to avoid very high analysis times on certain code.
  • Fixed evaluation of assignments in which one or several variables appear on both sides and a post increment operator appears on the right-hand side (e.g. i = A[i]++).
  • The list of files to exclude from the total coverage computation had not been stored on the server. This has been fixed.
  • Fixed handling of local settings to avoid that they are:
    • lost after upgrade to release 12.10,
    • overwritten when modifying an analysis with the same user from a different machine, or
    • not copied when creating a new revision of a project.
  • Fixed sporadic issues with the highlighting of failed assert directives that were inserted via the AAL annotation language.
  • Corrected some cases when the mapping to original sources was not working as expected.
  • Fixed unjustified messages about "definite runtime errors" that could occur in rare cases when the octagon domain was enabled.
  • Fixed the display of original source code in case of parse errors.