AbsInt Astrée and RuleChecker 18.10i b4387936

We are happy to announce build 4387936 of Astrée and RuleChecker release 18.10i.


Server and Client (User Interface):

* Corrected the behavior of the option –export-preprocessed such that
it exports the successfully preprocessed files even when
preprocessing of some files fails.

* File names in RuleChecker configurations are now exported to DAX
using relative paths.

* Improved the ALM token handling in case that the connection between
the a³ for C client and the analysis server is lost during
preprocessing. The rulechecker token is now released immediately as
soon as the server considers the connection definitely lost.

* Improved the ALM token handling in case of importing a DAX file
containing an <id> tag. The rulechecker token is now released after


* The analyzer now considers the ABI option bits_of_byte also when
determining the size of floats and doubles. In previous releases it
only had an effect on integer types. Therefore with sizeof_double=4
and bits_of_byte=16 the analyzer now considers doubles to have 64
instead of only 32 bits.

* Fixed an issue that caused the analyzer to abort with an error
message when using an undeclared absolute address of with an
incomplete type, e.g.,
struct T {}; // incomplete type …  struct T*
p = (struct T*)0x1000; // … used with absolute address

* Fixed an issue that in rare circumstances could stop the analyzer
with the error message “Cannot project mismatching partition IDs”.

* Fixed the display and reporting of unreachable if statements that
are partitioned by an __ASTREE_partition_control directive.

* Functions that are ignored due to an __ASTRE_ignore directive are
now displayed as filtered in the editor view.



* The new option collapse-multi-dimensional-arrays controls whether
multi-dimensional arrays are considered as a single type layer for
naming rule checks.

* The type name configured via option boolean-type is now equivalent
to _Bool for naming checks.

Rule Sets and Checks for C:

* Removed false alarms for the check array-initialization (rule
M2012.9.3) in case of nested arrays inside of zero-initialized
structures, such as struct { int a[2];} s = { 0 };

Rule Sets and Checks for C++:

* Improved precision of the check multiple-loop-counters

* Refined checks for rule M2008.4.5.3.

* Improved the check loop-control-modification for rule M2008.6.5.5.

* The new check float-suffix for rule M2008.2.13.4 warns about the
floating literal suffix ‘f’.

Qualification Support Kits

New test cases in the Astrée QSK:

* qk_directive_track_states

* qk_directive_merge_states

* qk_option_state_machine

* qk_option_automatic_state_machine

Please note that this release also contains the following changes, already shipped to Astrée customers with release 18.10i b3745084.


Server and Client (User Interface):

* Analyses that fail to start from the server’s analysis queue are no
longer automatically re-queued. This fixes issues with queued
analysis projects blocking the server.

* Fixed an issue in the installer that prevented the server from
starting automatically after reboot, even if the installer option
“Register a3 for C server as a service” was enabled.

* The context menu entries “Disable”, “Go to annotation” and “Edit” in
the editor now also work for AAL-inserted comment directives.

* Fixed the Verbosity selector of the Output view. In release 18.04 or
later, changing the verbosity in an already opened analysis project
could lead to the following undesired effects:
– empty cells in the ‘Message’ column of the Findings view
– missing information (message texts and data races) in XML and
custom report files that were generated after modifying the
verbosity slider.

Frontends and Preprocessor:

* Source directives are now also accepted and applied in single line
(‘//…’) comments.

* C and C++ and other stub library include paths moved to last
position of include paths. This allows to provide own standard
header replacements if needed. For example an own “math.h” will
overwrite the shipped stub library “math.h”.

* The C99 macro ‘__TIME__’ now expands to ‘??:??:??’ and ‘__DATE__’
now expands to ‘??? ?? ????’. This ensures stable results between
multiple analysis runs.

Integration with dSPACE TargetLink:

* Removed unintended output (state = ‘Hidden’) from the Matlab command


Pre-Release of the Finite State Machine Domain (due to popular demand):

* Added a new relational domain for more precise analysis of finite
state machines. The new domain is activated with the option
‘state-machine=yes’. It reacts to the new directive
‘__ASTREE_states_track((x))’ which indicates that ‘x’ is used to
encode the state of a state machine. Special treatment stops upon
encountering a directive ‘__ASTREE_states_merge((x))’ or
‘__ASTREE_states_merge(())’. The new option
‘automatic-state-machine=yes’ enables automatic detection of code
patterns used in state machine implementations, for which Astrée can
then insert ‘__ASTREE_states_track’ directives.

* Please note that this feature is currently still being tested and is
not yet covered by the QSK. It will be officially released in April
2019 (release 19.04).


* The analyzer is now faster on loops that contain
‘__ASTREE_partition_begin’ directives (improved widening).

* Improved the analyzers precision on computations with bit-masks.

* The heuristic selection of functions for context-insensitive
analysis (option ‘separate-function=*’) now takes function
substitutions into account. This results in a better choice of
separate functions in the presence of function substitutions.

* Improved analyzer performance for analysis projects that enable the
option ‘warn-on-field-overflows’.

* Improved the precision of location information for certain
alarms. In particular write data race and global assertion alarms in
an assignment are now reported for the left-hand side of the
assignment. Please note that comments for such alarms may need to be
moved to the new location when re-running older analyses.

* Fixed false alarms in ‘__ASTREE_modify’ directives on arrays.

* For function calls with incompatible parameter or return types, the
analyzer now assumes that values with incompatible type are
converted according to the rules of C, if such rules are
applicable. Otherwise it assumes any value.

* Control flow information is now also displayed if the reporting of
data flow information was disabled for the analysis (using the
option ‘dump-dataflow=no’). Moreover, it now also contains call
information for calls that are only reachable via separately
analyzed functions (option ‘separate-function’).

Bug Fixes:

* Fixed an issue in the evaluation of the directive
‘__ASTREE_partition_control((1))’. Using it in front of a loop
caused the first partition to get lost.

* Fixed an issue in the gauges abstract domain that could remove some
traces from the analysis, possibly stopping the analyzer with an
error message.

* Fixed address computation for objects that are specified to overlap
in memory by ‘__ASTREE_absolute_address’ directives.


Rule Sets and Checks for C:

* The new rule check ‘multiple-writes-in-full-expr’ warns about full
expressions in which a variable is written more than once to warn
about violations of rule M.12.2.

* Fixed essential typing of constant expressions in case that the ABI
value ‘bits_of_byte’ is set to a value other than the default value
8. This affects most M2012.10.x checks in case that the ABI is
configured in the aforementioned way.

* Alarms concerning essential types now also mention the type, not
just the category.

* The option ‘allow-signed-constant-with-unsigned’ is now also
considered for the check ‘bitop-type’ used in the rules CERT.INT.13,
CERT.INT.16, M.12.7, and X.A.5.40.

* Improved precision of the check ‘controlling-invariant-expression’
used in rule M.14.1, M2012.2.1, and M2012.14.3.

* RuleChecker now supports checking the following SEI CERT coding
rules/recommendations: CERT.API.8, CERT.ARR.1, CERT.ARR.39,

Rule Sets and Checks for C++:

* Improved precision of the check ‘inconsistent-default-argument’

* Improved precision of the check ‘null-as-integer’

* The new rule check ‘multiple-writes-in-full-expr’ warns about full
expressions in which a variable is written more than once to warn
about violations of rule M2012.13.2.

* Rule M2008.7.3.1 can now be parameterized with a set of type names
that are allowed to be declared at file scope.

* Improved the check for rule M2008.8.5.2 to eliminate false alarms
for empty initializer lists initializing the whole object, e.g. ‘int
a[2][2] = {}; // compliant’.

* The check ‘unused-internal-function’ (used in rule M2008.0.1.10) no
longer warns about template functions.

* The check ‘float-bits-from-pointer’ (used in rule M2008.3.9.3) now
also covers ‘reinterpret_cast’.

* The check ‘enum-usage’ (used in rule M2008.4.5.2) no longer warns if
the unary ‘&’ operator is applied to an expression of type ‘enum’.

Qualification Support Kits

Enhanced check for Microsoft Windows max path limitation.

New test cases in the RuleChecker QSK:

* qk_check_plain_char_operator

* qk_check_multiple_writes_in_full_expr

Linux 64-bit:


Windows 64-bit (self-installer):

Windows 64-bit (portable ZIP file version):

Installation and License Management

Double-click on the installer and follow the on-screen instructions.
During the setup, select both the a³ component and the AbsInt License
Manager (ALM) component. You need admin privileges for the installation.

a³ relies on DLLs from the Microsoft Visual C++ Redistributable
for Visual Studio 2017. The redistributable is included in the installer
as an optional component, or can be installed at a later point
from the directory share/3rdparty/vc.

Unpack the downloaded archive using unzip and change into the directory
it creates. There, run the shell script “install.sh” to install a³,
then run the script “install-alm-service.sh” to install the license server
and register it as a Linux service. You will need root privileges for this.

2. Please use your existing license file.
To activate it, first start the AbsInt License Manager.
Then open a web browser of your choice, go to the address
and select “Manage license” -> “Upload license file”.
The default administration password is “admin”.

3. Afterwards, start the a³ for C Server Controller, click on the “Start server”
button and select the server by double-clicking on the new entry in the
host name list. This will open a new window, in which you should see,
among other things, the line “No valid license specified”. Click on the button
to the right of that line to open the License dialog box. There, click on
‘Connect to license server…’ and choose one.

4. Your license is now activated and you can close the License dialog box.
After that, make sure that you’ve set a Data Directory. Only then will
a green dot appear in the Status field indicating that the a³ for C
server is running. Then you can close the a³ for C Server Controller
and start the a³ for C client.