We are happy to announce build 3593770 of Astrée and RuleChecker release 18.10i.
* Batch mode analysis runs now behave like GUI analysis runs
w.r.t. the printing of analyzer options in report files. That is,
only options that deviate from their default values are reported,
except if the new option print-all-options is enabled.
* The new option print-all-options=yes triggers printing of all
analyzer options, including those set to their default values.
* The tool now uses more descriptive names when referring to static
variables whose identifier is not unique. For example, a static
variable named “var” and declared in “file.c” is now reported as
* The new function metric LOCVAR counts the number of local variables
which are declared in a function.
* The LSCOPE metric now considers all function calls, dereferences,
array look-ups and struct-member accesses.
* The generated HTML report files now contain a table of contents to
allow for easier navigation in large report files.
* The C frontend now accepts lvalue casts, as supported by older
versions of the GCC compiler. Here is an example:
float* fp = 0;
int* ip = 0;
(int*)fp = ip; /* lvalue cast */
Note that such code violates the diagnostic rule A.2.6 (check
lvalue-cast) and is no longer supported by current C compilers.
* The C frontend now rejects strictly invalid array index expressions
(which are also not accepted by compilers).
* Improved speed of filtering and searching in large collections of
findings, e.g., in the Findings view.
* Improved performance when displaying source files with large numbers
* Fixed the Watch view for investigating variables and lvalues in
Astree. The feature was not working correctly in release 18.10.
* Jumping to another code location or switching from an editor to
another view now always enables the button for going back to the
last code location.
* When the second argument of a shift is too big (alarm “range of
second shift argument … not included in …”), the analyzer now
also includes 0 in the result.
* Modified the syntax of the following directives to improve
NEW SYNTAX OLD SYNTAX
__ASTREE_volatile_input((v; [l,h])); | __ASTREE_volatile_input((v, [l,h]));
__ASTREE_global_assert((v; [l,h])); | __ASTREE_global_assert((v, [l,h]));
__ASTREE_known_range((v; [l,h])); | __ASTREE_kown_range((v, [l;h]));
__ASTREE_partition_ranges((g; [l,h], [l,h])); | __ASTREE_partition_ranges((v: [l;h], [l;h]));
The new syntax is preferred although the old syntax is still accepted.
* DAX files containing the option
where ‘any-relational-domain’ is the option key of any relational
domain, e.g., ‘octagon’, are now rejected with an error message. In
previous releases, such specifications were accepted but lead to a
different behaviors in GUI and batch mode.
* Alarms about possible data races now include the name of the process
in which the alarm is detected.
* The analyzer no longer stops with an error if the return type of a
function is not compatible with the return type assumed by the
calling expression and the result of the function call is not
used. Instead, the analysis raises an alarm A and continues. The new
behavior is consistent with the behavior for incompatible function
calls in which the result is used by the caller.
* Contexts proposals for program slicing no longer contain contexts
that have not been reached by the runtime error analysis.
[RuleChecker for C]
* Removed false alarm for check pointer-qualifier-cast-const-implicit
in case that the second argument to __astree_memcpy is a pointer to
* Removed false alarms for the check boolean-invariant in switch
* The check function-pointer-cast for rules M.11.1 and M2012.11.1 no
longer warns about null pointer constants.
* Improved the checks multiple-volatile-accesses and evaluation-order
so that they no longer raise false alarms when taking the address of
* Each of the following checks has been split into a check for
const-qualified objects and one for non-constant objects:
global-object-name => global-object-name and global-object-name-const
static-object-name => static-object-name and static-object-name-const
local-object-name => local-object-name and local-object-name-const
* Added the new rule T.15.1 which is associated with the check
max-local-variables. This check is violated if the specified
threshold for local variables in a function is exceeded.
* Added the new rule T.16.1 which is associated with the check
max-size-of-statement. This check is violated if the specified
threshold for the sum of operands and operators in a statement is
* Improved precision of the check parameter-missing-const for rules CERT.DCL.0, CERT.DCL.13, M.16.7, and M2012.8.13.
[RuleChecker for C++]
* Improved precision of the following checks:
* Improved precision of the check plain-char-usage in code using the
comma operator or references.
* Improved precision of the check underlying-cvalue-conversion by
ignoring irrelevant implicit conversions like, e.g., “non-const” to
* The check functional-cast no longer reports constructor conversions.
* The checks new-operator and delete-operator no longer warn about
* The check unary-assign-separation is now also applied to overloaded
* The checks for rule M2008.6.4.3 no longer warn about switch
statements without default clause.
* The checks for rule M2008.6.4.6 no longer warn about exhaustive
switch statements over values of enum type without default clause.
* Improved the check functional-cast for rule M2008.5.2.4.
* Sharpened the check bitop-type to warn about more cases of bit
operations on values of unfitting type.
* The check cast-integer-to-pointer now warns when casting an integral
type to any pointer type.
* The check integral-type-name now also warns about uses of integral
type names in cast operators.
[Integration with dSPACE TargetLink]
* The AbsInt toolbox for TargetLink can now be configured to run the
analysis in batch mode instead of running it in GUI batch mode. The
analysis then runs without any user interaction and without opening
[Qualification Support Kits]
* Added missing text fragments to the Verification Test Plan for a³
(RuleChecker) for C concerning the QSK tests qk_check_extra_tokens
* New test cases in the Astrée QSK:
* New test cases in the RuleChecker QSK:
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.