Astrée and RuleChecker release 18.10i

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

Release Notes:
=============

[General]

* 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
var@”file.c”.

* 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.

[Frontends]

* 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).

[Client GUI]

* 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
of alarms.

* 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.

[Astrée]

* 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
consistency:

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
no
followed by
yes
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
const.

* Removed false alarms for the check boolean-invariant in switch
statements.

* 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
an array.

* 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
exceeded.

* 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:
– address-of-overload
– digraph-token
– stdlib-use
– unrelated-pointer-conversion
– unary-assign-separation
– virtual-call-in-constructor
– return-position

* 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
“const” pointers.

* The check functional-cast no longer reports constructor conversions.

* The checks new-operator and delete-operator no longer warn about
placement operators.

* The check unary-assign-separation is now also applied to overloaded
operator calls.

* 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
any windows.

[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
and qk_check_non-standard_identifier.

* New test cases in the Astrée QSK:
– qk_option_print_all_options
– qk_option_drop_unused_statics
– qk_option_filter_attributes

* New test cases in the RuleChecker QSK:
– qk_check_global_object_name_const
– qk_check_local_object_name_const
– qk_check_static_object_name_const
– qk_option_print_all_options
– qk_option_file_name_modifier

Linux 64-bit:
https://www.absint.com/dla/2018/10i/5ab356a7e12/a3_c_linux64_b3593770_release.zip
md5-file:
https://www.absint.com/dla/2018/10i/5ab356a7e12/a3_c_linux64_b3593770_release.zip.md5
md5-sum:
9366c9a56f6e68a5f5272a548fc7bdff

macOS:
https://www.absint.com/dla/2018/10i/5ab356a7e12/a3_c_darwin64_b3593770_release.zip
md5-file:
https://www.absint.com/dla/2018/10i/5ab356a7e12/a3_c_darwin64_b3593770_release.zip.md5
md5-sum:
e0776babf74cecce2d1fa45f267f373a

Windows 64-bit (self-installer):
https://www.absint.com/dla/2018/10i/5ab356a7e12/a3_c_win64_b3593770_release.exe
md5-file:
https://www.absint.com/dla/2018/10i/5ab356a7e12/a3_c_win64_b3593770_release.exe.md5
md5-sum:
1e07acd04600af292359c0701c9c30f6

Windows 64-bit (portable ZIP file version):
https://www.absint.com/dla/2018/10i/5ab356a7e12/a3_c_win64_b3593770_release.zip
md5-file:
https://www.absint.com/dla/2018/10i/5ab356a7e12/a3_c_win64_b3593770_release.zip.md5
md5-sum:
a79f53df9a0727b7ae06f0ca15403bb2

Installation and License Management
===================================

1. WINDOWS:
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.

LINUX:
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
http://localhost:42425
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.

2018-11-20T01:15:43+00:00