AbsInt Failure Notices: Astrée for C

Failure notice #27321 for Astrée.

The reported issue will be fixed with release 19.10.

[Failure Notice #27321]

Problem Description:

—————————

The ABI option ’rounding_mode=to_nearest’ causes unsound results.

Scenario:

———

Switching the ABI option ’rounding_mode’ to the non-default value ‘to_nearest’ leads to unsound evaluation of conditional expressions with floats and doubles. Here is an example that shows an affected expression:

if ((float)0.1 > 0.0)

Symptoms:

———

1) In the example above the analyzer prints a message “Direct flow changed to _|_ during test in this context”.

Release 19.04 and later report this text as an error message.

Older releases report it as a notification message.

As a consequence of the error, the analyzer stops at this program point in this context.

2) Depending on the form of the expression and the assumed values of its operands, the analysis may also continue.

In this case, the analyzer may miss reachable program paths and/or assume invalid ranges for some variables.

As a consequence, the analyzer may fail to report defects.

Affected versions:

——————

Release 15.04 and later.

Troubleshooting:

——————

Change the ABI option ’rounding_mode’ to its default value ‘all’ or upgrade to a corrected version of Astrée (19.10 and later).

www.absint.com

2019-10-09T15:41:59+00:00