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.



==============================================================================
Last modified on 19 April 2013 by alex@absint.com.
Copyright 2013 AbsInt. http://www.absint.com/
==============================================================================
An HTML version of these release notes is available at
http://www.absint.com/releasenotes/astree/13.04/