Astrée Release 14.04

New features
* The XML reports of different analyses or different versions
  of the same analysis can now be compared with respect to options,
  directives, source files, and numbers of alarms and errors,
  using the XML differences viewer which is available from the
  tools menu. The differences viewer can also be accessed from
  the analysis history dialog to inspect the differences between
  different revisions of an analysis.

* The analyzer can now detect and warn about write accesses
  to variables which are possibly not read between two write accesses
  (write-after-write). This feature is controlled by the new option

* The GUI can now save the project configuration in a DAX file.
  This feature is available via "Project" -> "Export" -> "Project...".

* The new External Declarations view allows to specify types
  and (function) declarations that are missing, e.g. because
  they are part of compiler-specific extensions, or because
  some include files are not available to the analyzer.

  One use case for this feature is for generating stub functions
  for compiler intrinsics. When providing the analyzer with a suitable
  function declaration via the External Declarations view,
  it can automatically generate a stub function if the option
  "auto-generate-stubs" is used.

* The new directive "__ASTREE_partition_ranges((e:a1,...,an))"
  allows partitioning an expression "e" according to a list
  of intervals "a1,...,an". The alternative syntax
  automatically generates partitions covering the range
  of the expression "e1" using the minimal size specified by "e2"
  and/or the maximum number of partitions "n".

* The detection of shared variables has been improved
  so that it is now possible to have two tasks using the same
  entry function. This brings about a modification of the
  __ASTREE_asynchronous loop directive, which now
  requires all tasks to be listed explicitly. Hence, analysis
  wrappers of the following form are no longer valid:

    typedef void(*t)(void);                                
    static t tasks[] = { t1, t2 };                         
    unsigned int idx;                                      
    __ASTREE_known_fact(( idx < 2 ));                      
    __ASTREE_asynchronous_loop(( tasks[idx]() ));          

  The correct way for re-writing the above analysis wrapper example is:

    __ASTREE_asynchronous_loop(( t1, t2 ));                

  The wrapper generator in the GUI has been modified accordingly.

* Fixed the AAL processor so that it allows inserting
  "__ASTREE_partition_control" statements before assignments.

* Fixed the calculation of coverage information and number of statements
  for analyses that use the option "auto-generate-stubs=yes".

* Improved the precision of the analyzer on barycentric computations
  of the following form:

    in1 = [-1.1];
    in2 = [-1,1];
      while (1) {
        b = [0,1];
        out = b * in1 + (1 - b) * in2;
        if (*) in1 = out;
        if (*) in2 = out;

* Astrée now issues an alarm when an expression may write
  to a string literal in which case the behavior is undefined
  and the program may even crash. Here is an example:

    char *s = "Sky";
    s[0] = 's';

  The result of Astrée:

    ALARM (A): write to constant: writing to string literal "Sky".
    Definite runtime error during assignment in this context.
    Analysis stopped for this context.

* If an AAL annotation cannot be inserted, the analyzer no longer stops
  but reports an error message and continues with the analysis.

* The precision of the domain of boolean relations has been improved.
  In particular, the analysis of guards in tests is now more precise.

* The option "cut-invalid-pointer" has been removed.

* The new expert option "dump-hypotheses=[yes|no]" controls whether
  the analyzer output contains additional sections that list all
  semantic hypotheses and further directives. It is provided so that
  the size of the analyzer output can be reduced when running analyses
  with very large numbers of directives. However, it is recommended
  to leave the option enabled so that the result documents the semantic
  hypotheses on which the correctness of the analysis result relies.

* Improved the precision of the analyzer when analyzing conditional
  expressions using the bitwise OR operator.

* Improved precision on pointers when casting them as integers.

* Initialization of global variables to 0 can now be activated independently
  of the initialization option for static variables. That is, even with
  "static-initialization=no" and "global-initialization=yes",
  the non-static global variables will now be initialized to 0.

* Modified the automatic wrapper generator for TargetLink so that
  the root step functions of the model can be called in arbitrary order.

* The text search feature of the GUI can now also search the original
  source files, not only the preprocessed files.

* Modified the filtering (Ctrl+F) in the Summary/C view so that filters
  now consider the names of the categories, not the alarm messages.

* Modified the filtering (Ctrl+F) in the Summary/F view so that filters
  now consider the names of the files, not the alarm messages.

* A new standard example demonstrates automatic detection
  and sound analysis of shared variables in asynchronous tasks.

* Filtered expressions are now highlighted in the editor
  also when the analysis was not successful.

* The original source files of an analysis project can now be downloaded
  from the server from the context menu of the original files list.

* Re-designed the preprocessing dialog of the GUI to improve usability,
  performance, and flexibility.

* Fixed sporadic crashes when deleting configurations
  from the Preprocessing view.

* Improved warning message when some reports could not be generated.

* It is now possible to reorder the entries in the Parser view using
  drag and drop.

* Improved performance and reduced memory consumption when loading
  information about not analyzed code in the client.

* A tooltip in the Coverage column of the Summary/F view now displays
  the number of statements that were not analyzed, together with
  the total number of statements in the file.

* The Alarm density view can now be filtered such that it displays
  only functions with more alarms than a given threshold.

* Fixed the automatic upload of original source files to the server
  after preprocessing. Instead of uploading only the C files from the list
  of files to preprocess, it now also uploads all included header files.

* Locating the original source files for large analysis projects
  is much faster now.

* Fixed a bug that could cause the upload of original source files
  to overwrite some of the preprocessed files on the server.

* The uploading of source files to the server has been optimized
  to reduce transfer times.

* Reduced server startup time on working directories with many large projects.

* Improved the error message for client/server connection failures
  due to version mismatch.

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