AbsInt Failure Notices: Astrée for C

[Failure Notice #26097]

Problem Description:
——————–
Enabling the gauge domain may cause the analyzer to assume incomplete value ranges for expressions that involve type-punning. As a consequence, reachable program paths may be considered unreachable and the analyzer may fail to report true alarms.

Scenario:
———
If all of the following conditions are fulfilled

– the gauge domain is enabled (gauges=yes),
– the analyzer evaluates an expression that involves type-punning,
– the source type is signed and of smaller size than the destination type, then the assumed value range for the result of the expression may be incomplete.

In the example below, a 4-byte signed char array is read as one 4-byte signed int. Assuming a 32-bit little-endian ABI, possible results are 0 or 32768. The analyzer falsely assumes that the result is strictly 0, hence the then-branch of the if-statement is considered unreachable.

Whether the erroneous behavior is triggered depends on the possible input value ranges. After evaluating the expression, the analyzer may either assume the correct result, stop with an error, or continue with incomplete result.

Please note that the gauge domain is enabled by default since release 18.10 b3429976.

Example:
struct S { signed char c[4]; };
struct S s = { {0, -128, 0, 0} };
if (maybe)
s.c[1] = 0;
if (*((signed int*)&s.c))
/* then-branch not reached with ‘gauges=yes’ */

Affected versions:
——————
All versions released since April 2016, starting with release 16.04 b262856. In all versions released since October 2018, starting with release 18.10 b3429976, the gauge domain is active by default.

Troubleshooting:
—————-
Disable the gauge domain (gauges=no). Analyses of code that does not contain expressions that involve type-punning, are not affected by this issue.

———————————————————————

———————————————————————

[Failure Notice #26110]

Problem Description:
——————–
Comparing a pointer with NULL returns strictly false for pointers that may point to NULL or to absolute addresses.

Scenario:
———
If at some program point a pointer may only
– be a NULL pointer, and
– point to absolute addresses or variables with declared absolute addresses, then the analyzer falsely assumes strict inequality with NULL when testing that pointer for equality or inequality with NULL.

The issue does not occur if the pointer may also point to a program variable for which no absolute address has been declared.

Example:
int* null_or_absolute_address(void)
{
if (maybe)
return 0x1000; /* any absolute address */
else
return 0;
}
void f(void)
{
int* p = null_or_absolute_address();
if (!p)
/* then branch not reached */
}

Affected versions:
——————
All versions released since April 2014, starting with release 14.04 b217166.

Troubleshooting:
—————-
Analyses of code that does not assign absolute addresses to pointers, or never tests such pointers for equality or inequality with NULL, are not affected by this issue.

There is no workaround by means of changing configuration parameters of the analyzer. To achieve full coverage, affected NULL-pointer tests need to be rewritten using explicit casts, e.g:

if (!(size_t)p)
/* explicit cast makes then-branch reachable */

Please note that this workaround can lead to false alarms, because the analyzer will not remove NULL from the possible values assumed for the tested pointer.

———————————————————————

———————————————————————

[Failure Notice #26130]

Problem Description:
——————–
Arithmetic operations with enum types may yield wrong results if using the ABI option ‘enum_preferred_size=smallest’. As a consequence, reachable program paths may be considered unreachable and the analyzer may fail to report true alarms.

Scenario:
———
Arithmetic operations yield wrong results if
– the ABI option ‘enum_preferred_size=smallest’ is used
– the operation is performed with an enum type that can be represented by an integer type smaller than ‘int’
– the operation overflows the range of that smaller type.

In the example below, the left-hand side of the if-condition left-shifts a small enum type that fits into ‘signed char’, such that it overflows the ‘signed char’ range. The right-hand side of that comparison performs the same operation in ‘signed int’. The analyzer falsely concludes that the results are not equal and consequently considers the then-branch of the if-statement unreachable.

Example:
enum E { A = 1 };
if (A << 7 == 1 << 7)
/* then branch not reached with ‘enum_preferred_size=smallest’ */

Affected versions:
——————
All versions released since October 2013, starting with release 13.10 b208628.

Troubleshooting:
—————-
Analyses that use the ABI option ‘enum_preferred_size=int’ are not affected by this issue.

Analyses that use the ABI option ‘enum_preferred_size=smallest’ should be re-run with all overflow warnings on integer types enabled:
warn-on-integer-arith-ranges=yes
warn-on-integer-lshift-ranges=yes
warn-on-signed-integer-lshift-ranges=yes

If no overflow is reported for an arithmetic operation on an enum type, the analysis is not affected by this issue.

———————————————————————

2019-04-03T13:37:40+00:00