Astrée Release 17.10
--------------------


New comment mode
----------------
Alarms reported by Astrée can now be commented on using code patterns
rather than AAL annotations. While the latter are more precise (as they 
identify code locations unambiguously), code patterns can be very useful 
for keeping track of alarm comments in projects with significant code changes
between analyzed revisions, notably when using code generators.

The default commenting mode for new projects can be set under 
Project → Preferences → General → Findings.

For existing projects, the default mode is AAL. It can be changed, 
but any existing comments need to be transferred manually.


Faster performance
------------------
▲ The analyzer is now substantially faster by default. In some cases 
  this can lead to less precise results. To reset precision to previous 
  levels, use the new option widening-with-thresholds=yes.
▲ The integrated preprocessor now performs better as well.


Higher precision
----------------
▲ The analysis is now more precise for expressions that involve arrays 
  and occur inside of loops.
▲ Improved the precision of the octagon operations on divisions. 
  Operations such as x/y when 0 < x < y are now inferred 
  to be smaller than 1.
▲ Improved the heuristics for double if partitioning and increased 
  the threshold for aggressive array index partitioning. 
  This modification fixes precision regressions that have been observed 
  on certain code with release 17.04.
▲ Optimized the loop caching heuristic (controlled by the option 
  cache-iterates) to make better choices when selecting loops for caching.
  This may increase analysis precision as well as reduce memory consumption.


Other improvements
------------------
▲ The tick character ' can now be used in filter patterns and replacements.
▲ The notifications about ambiguities due to side effects in expressions 
  or initializers, and the option warn-sideeffects that controlled such 
  notifications, have been removed. They are replaced by the two diagnostic 
  rules A.4.1 and A.4.2 and their respective checks evaluation-order and 
  evaluation-order-initializer.
▲ When starting a client using alauncher, a temporary server 
  can be started in the background using the new option --temp-server.
  The client automatically connects to that server and the server is 
  shut down when the client process stops.


Qualification Support Kits
--------------------------
▲ Under Windows, the maximum path length limitation is now checked 
  every time a test case is loaded.
  
▲ Four test cases have been added:

  △ qk_aal_comment_annotation_alarm
  △ qk_option_max_finite_int_set_size
  △ qk_option_warn_on_subsequent_uninitialized_reads
  △ qk_option_widening_with_thresholds

▲ The test case qk_option_warn_sideeffects has been removed, 
  as it is now covered by new test cases in the RuleChecker QSK.


Windows support
---------------
Since release 16.10, Astrée relies on DLLs from the Microsoft Visual C++ 
Redistributable for Visual Studio 2017. Starting with this release, 
the redistributable is included in the installer as an optional component,
or can be installed manually at a later point from the directory 
share/3rdparty/vc.


C frontend
----------
▲ Added support for:

  △ GCC's __alignof__ and the C11 feature _Alignof.
  △ the C11 feature _Static_assert
  △ constant expressions in array member designators of offsetof()
  
▲ The frontend now prints an error message when __ASTREE_trash 
  or __ASTREE_access are accidentally used with a non-pointer variable.
▲ The frontend now accepts multi-character character constants 
  and handles them like GCC, i.e. as digits to the base UCHAR_MAX+1.
▲ The frontend now allows sizeof(*x) when *x has type void. 
  The result of this operation is 1, which corresponds to how GCC behaves.
▲ Modified the way in which static variables and functions are renamed 
  by the analyzer to resolve naming collisions when linking translation 
  units into a global program representation. 
  The new renaming scheme uses much shorter, and more stable, names.
  A static function or variable X may now be renamed into 
 "__ASTREE_static_X_8" 
  where 8 is a stable ID for the file in which X is defined. 
  Previous versions of Astrée used to rename X into something like 
 "X__ASTREE_drive_C_users_john_doe_analysis_tmp_fileX_c_3487463"
▲ Inline functions with external linkage are now represented 
  by a single definition.
▲ The frontend now retains type qualifiers when using typeof 
 (GCC extension). This modification can affect rule checking 
  on typeof expressions involving qualified types.
▲ The tool now also notifies about ambiguities due to side effects 
  in expressions or initializers whenever an object is modified 
  multiple times between two sequence points.
▲ Fixed the concatenation of two string literals in the case that 
  the first string literal ends in an escape sequence.
▲ Fixed the parser filter for the case of applying several filters
  to immediately adjacent characters.
▲ Fixed handling of source files with inconsistent line endings.


Original-source frontend
------------------------
▲ Suppress and comment directives in source file comments 
  now also support negative offset/length values.
▲ Fixed the parser for original source files to allow 
  the character sequence ?\ inside of string literals.


Project bar
-----------
▲ File lists can now be filtered by pressing Ctrl+F.
▲ The new Information view displays general project information 
  such as name, type, and revision.
▲ The Welcome view is no longer accessible from here. 
  It only opens on startup and can later be accessed via the Help menu.


ABI configuration view
----------------------
Corrected cases when the  ABI values pointer_attributes_1, 
pointer_attributes_2, and pointer_attributes_3 were not reset.


Rules configuration view
------------------------
▲ After importing RuleChecker configurations, the configuration list 
  in the Rules tab now automatically expands with the most recently 
  imported configuration selected.
▲ Reorganized the context menu in the Rules configuration view 
  to improve usability.


Preprocessor view
-----------------
▲ Improved the display of the preprocessor output.
▲ The automatic resolution of include paths has been improved 
  for projects with multiple preprocessing configurations.
▲ Improved the display of error messages that may be raised 
  during the processing of OIL files for OSEK configuration.


Function locations
------------------
The Analysis entry view and the list of function metrics under 
Overview/Metrics now also display the code location (file name, 
line, and column in the preprocessed code) for each displayed function.


Findings view
-------------
The list of message contexts displayed when selecting a finding can now 
be searched, e.g. to find the contexts with a definite runtime error. 
Simply press Ctrl+F when the list of message contexts is in focus.


Further changes
---------------
▲ Improved the upload of original source files to the server 
  to handle analysis projects with a very large number of source files.
  
▲ The value of the option config-file is no longer modified 
  by the DAX export and the corresponding *.cfg file can be downloaded 
  without renaming. The DAX export dialog allows selecting the source files
  to be downloaded.
  
▲ The built-in preprocessor is now disabled when creating a new project 
  from already preprocessed files using the new project wizard.
  
▲ Fixed the wrapper generator so that it produces correct code even if 
  the user-specified task list has gaps (for example, tasks are specified 
  in line 1 and 3, while line 2 is left empty).
  

Extensions of the DAX format
----------------------------
▲ The commenting mode can be specified in the root element using 
  the attribute comment-mode="AAL" or comment-mode="patterns".

▲ The element <annotations> now supports the attribute "import".

▲ The new comment patterns can be specified in DAX in the following manner:

  <annotations>
    <comment-pattern classification="..." type="...">
      <comment/>
      <file/>
      <ofile/>
      <oline/>
      <function/>
      <expression/>
      <abstract-expression/>
      <abstraction/>
     <context/>
    </comment-pattern>
  </annotations>

  The exact contents of the tags are defined by the analyzer's internal 
  comment abstraction which can be exported into DAX from the GUI.


Options
-------
▲ New options:

  △ warn-on-subsequent-uninitialized-reads 
    controls whether subsequent reads of uninitialized reads are reported. 
    The option is active by default which corresponds to the behavior 
    of older Astrée releases.
  
    If the option is disabled, Astrée will raise only one 
    uninitialized read alarm on the following example code, 
    whereas with default settings two alarms will be reported:

      void main(void)
      {
        int i;
        int a = i;
        a = a & i;
      }

  △ max-finite-int-set-size=n 
   (default 0) controls the domain of finite integer sets which can improve 
    analysis precision on integer values.
    
  △ drop-unused-statics 
    controls whether the analyzer omits unused static functions 
    from the coverage information. Enabled by default.
    
  △ widening-with-thresholds 
    enables a more precise but also more costly analysis. 
    Disabled by default.

▲ The heuristic for the context-insensitive analysis of functions 
  can now be extended by a list of functions that shall not be analyzed 
  in a context-insensitive manner. 
  For example, the option separate-function=*,-f enables the heuristic 
  but ensures that the function f is not analyzed context-insensitively.


Directives
----------
▲ __ASTREE_ignore directives no longer need to be preceded 
  by a definition of the respective function. The return value 
  of an ignored function is now considered initialized.
  
▲ The syntax for expressing array slices has been changed 
  from [lo-hi] to [lo..hi].
  This affects directives such as __ASTREE_modify. 
  Notifications will be issued when the deprecated syntax is used.


Stub libraries
--------------
▲ Modified the OSEK stubs to avoid possible name clashes 
  with user-defined resources in OIL files.
▲ Modified the OSEK stub library so that task and alarm identifiers
  can be used in constant expressions. Users that override the TASKNAME macro
  must now also override the TASK macro.
▲ The function pow() in the example C stub library has been generalized 
  to also return negative values.


Server and server controller
----------------------------
▲ Clients can now be disconnected via the server controller's Clients view.
▲ The server controller now also displays the license features 
  for analyzers running on a server. This makes it easier to recognize 
  whether a server is configured for Astrée, RuleChecker, or both.


Integration with TargetLink
---------------------------
▲ Added support for TargetLink 4.2.
▲ The Toolbox now supports the new Astrée preference 
 "Use comment patterns".
▲ The latest version of the Toolbox can now be used with older versions 
  of Astrée/RuleChecker, specified under Astree → Preferences.


XML report
----------
The XML result file now includes the analysis project's <name>, 
<description>, and <revision> number.


Slicing
-------
The program slicer now supports selecting a specific call context,
i.e. a series of function calls leading to the program location 
of the selected slicing criterion. This new feature is most useful 
when deriving a sub-program to investigate runtime errors reported 
in a certain call context.


Wrapper generator
-----------------
▲ Wrapper code generated by the built-in wrapper generator suppresses 
  alarms about missing parameters in function calls. Initialization and 
  periodic functions can be intentionally called without arguments to let 
  the analyzer run with conservative assumptions about the missing parameters.
▲ The wrapper generator now introduces additional variable declarations 
  to facilitate project setup.


Improved handling of invalid function calls
-------------------------------------------
▲ Astrée no longer stops with an error when a function is called 
  with too few arguments. Instead an alarm is raised, and the analysis 
  continues with the assumption that the missing parameters are initialized.
  
▲ Likewise, the analyzer no longer stops with an error for function calls 
  that provide too many arguments. Instead the runtime error is reported 
  and the analysis continues while ignoring any excess arguments.
  
▲ The analyzer no longer stops in function calls with mismatching types 
  that can't be resolved by type promotion or a reinterpretation of values. 
  In these cases the analyzer issues an alarm of the form 
 "ALARM (A): invalid function call" 
  and continues with the assumption that affected parameters 
  of the function have arbitrary values.
  
▲ When a function is called via an invalid function pointer, 
  Astrée no longer stops but instead assumes that the function call
  may be to an unknown function that returns an arbitrary value.
  
▲ In a function call with an incompatible return type that cannot be
  reinterpreted, the analyzer no longer stops with a definite runtime error.
  Instead it assumes that the return value is the full range of the expected
  result type or INVALID if the expected result type is a pointer.


Messages and warnings
---------------------
▲ Enabled suppression and commenting of analyzer alarm messages 
  when running the analysis in parallel mode.
▲ The analyzer no longer displays duplicate warnings for overlapping 
  undeclared absolute addresses.
▲ Fixed false alarms for correct uses of arrays with only tentative 
  definitions.
▲ Fixed a client crash during report generation in batch mode 
  that could be triggered by report configurations that contained 
  a list of analyzer messages grouped by category.


Other changes
-------------
▲ Shortened the "incompatible types in function call" prefix 
  of some alarms to "invalid function call".
  
▲ Linking overlapping absolute addresses no longer depends 
  on the order of declarations.
  
▲ Added support for overlapping memory blocks (at absolute addresses)
  with volatile input specifications. In such cases, the effective 
  volatile range for any part of such memory is the join of all 
  overlapping volatile input specifications.
  
▲ When calling a function with too few arguments while having
  the option assume-unknown-pointers-are-valid enabled, Astrée 
  now assumes that these parameters may point to valid memory locations, 
  thus continuing the analysis even when they are dereferenced.

▲ It is now possible to read absolute addresses encoded in char arrays 
  to initialize pointers. Example:
  
    unsigned char mem[] =
      { 0, 0, 0, 0x2A, 0, 0, 0x10, 0x0C,
        0, 0, 0, 0x17, 0, 0, 0x05, 0x39, };
    __ASTREE_absolute_address((mem, 0x1000));
    
    typedef struct A { int  a; int* b; int  c; } A;
    
    int main(void) {
      A* p = (A*)0x1000;
      /* now Astree knows precise values for all members of 'p'
         including that p->b points to 0x100C */
    }

▲ Partial initializers for variables of type struct with flexible 
  array member are now supported.

▲ The analyzer now supports the interpretation of pointers as enum values.
  Code like the following can now be analyzed:

    enum E { A } e = (int*)0;

▲ When raising an invalid dereference due to offset overflow, 
  e.g. by using a potentially-too-large value as array index, 
  Astrée now removes all incorrect offsets, rather than a select few. 
  This prevents undesired subsequent alarms following an invalid dereference 
  due to incorrect offsets.

▲ When generating absolute addresses, Astrée now limits what addresses 
  are valid based on the size of pointers declared in the ABI.

▲ Astrée now fully supports GCC extended assembler statements, 
  i.e. it soundly approximates all reads and writes on program variables, 
  as specified by the extended assembler syntax.

  
Bug fixes
---------
▲ Fixed the file filter for rule violations configured in Overview → 
  Findings or the custom report configuration. It previously had no effect 
  on the lists of findings displayed in the Findings view or the custom 
  report files, respectively.
  
▲ Fixed an analyzer crash when using variables with overlapping 
  absolute addresses containing volatile parts while having the option 
  volatile-global or volatile-static enabled.
  
▲ Fixed exceptional aborts of the analyzer that could occur 
  when enabling the option separate-with-caller-stack-pointers.
  
▲ Fixed an exceptional abort of the analyzer that could occur 
  when analyzing asynchronous programs.
  
▲ Fixed an issue that could cause the analysis to not terminate 
  when enabling the octagon domain on code with recursive function calls.
  
▲ Fixed cases of missing or incomplete invariants collected 
  with the option export-invariant and displayed in the watch window.
  
▲ Fixed an issue that could cause the analyzer to stop 
  with the error message "Failure(‘Wrong type for a struct')".
 
▲ Fixed an issue that could cause modified analysis settings 
  to get lost when hitting the analysis start button.


RuleChecker
See the dedicated release notes for RuleChecker 17.10 at 
www.absint.com/releasenotes/rulechecker_release_1710.html.


------------------------------------------------------------------------------
Last updated on 19 October 2017 by alex@absint.com. Copyright 2017 AbsInt.
------------------------------------------------------------------------------
An HTML version of these release notes is available at
www.absint.com/releasenotes/astree/17.10