AbsInt Failure Notices: Astrée for C

We hereby notify you about 3 failures in Astrée. The reported issues will be fixed with the next intermediate release.

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

[Failure Notice #26640]

Problem Description:

——————–

The analyzer fails to report certain run-time errors in the left-hand side of a binary operation, depending on the form of the operands.

Scenario:

———

The analyzer fails to report certain run-time errors in the left-hand side of binary operations if the operands have the following form:

– the left-hand side is free of side effects

– the right-hand side is an expression containing one of the

following operators: !, !=, ==, <, >, <=, >=, &&, || Affected run-time errors are at least arithmetic overflows, NaN or infinity float arguments, and invalid shift arguments.

The following examples illustrate the failure:

1) Overflow in ((char)x) is not reported:

int x = 1000;

int y = ((char)x) + (x <= 128);

2) Overflow in (x + 1) is not reported:

int y = 1;

int x = 2147483647;

int z = (x + 1) – (x && y);

3) NaN or infinity float argument (a) is not reported:

d = (a) * b * !c;

Please note that the analyzer only omits the alarm message. It still computes sound results for affected expressions.

Affected versions:

——————

All

Troubleshooting:

—————-

There is no workaround for the issue.

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

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

[Failure Notice #26626]

Problem Description:

——————–

Write actions via analyzer directives or built-in functions are not always taken into account in separate functions and parallel processes.

Scenario:

———

1) If a process uses a shared variable as an argument to certain

analyzer directives or built-in functions which write to that

argument, the effects do not become visible in other parallel

processes.

2) If a function in a separate context (i.e. the root of the context

is a context-insensitively analyzed function) uses a non-local

variable as an argument to certain analyzer directives or built-in

functions which writes to that argument, the effects do not become

visible in the contexts calling the separate context.

Affected directives and functions are:

– __ASTREE_modify((shared_var; [min, max]));

– __ASTREE_modify((shared_var; full-range));

– __astree_bzero(shared_var, sz);

Please note that the issue also affects the memset stub, shipped with the tool as part of the C standard stub library, if it sets memory to 0. Other stub functions are not affected.

Here is an example that illustrates the first scenario.

int shared = 1;

void process1() {

__astree_bzero(shared, sizeof(int));

}

void process2() {

int x;

x = shared;

}

void main() {

__astree_create_process(process1, 1, 2);

__astree_create_process(process2, 2, 1);

__astree_start_process(1);

__astree_start_process(2);

}

The value of ‘x’ in ‘process2’ is 1, whereas it should be [0,1]. The data-race on the variable ‘shared’ is not reported.

Here is an example that illustrates the second scenario.

int x = 3, y=3;

void f() {

__ASTREE_modify((x; [0,1]));

y = x;

}

void g() {

f();

__ASTREE_assert((x == 3));

__ASTREE_assert((y == 3));

}

The assertion ‘x==3’ is assumed to hold (no alarm) if using the option ‘separate-function=f’. Note that the assertion ‘y==3’ is correctly reported to fail.

Affected versions:

——————

All versions since release 15.04 which introduced the affected features.

Troubleshooting:

—————-

Possibly affected are all analyses that

– use an asynchronous setup with parallel processes or that enable a

context sensitive analysis by providing a non-empty argument to the

option ‘separate-function’, and

– contain uses of the affected directives and built-in functions in

functions that are called by parallel processes or separately

analyzed functions.

As a workaround, exclude functions with affected directives from separate analysis or replace affected directives as follows:

1) __ASTREE_modify((v; [lb, ub]));

=> __ASTREE_modify((v));

__ASTREE_known_range((lb <= v && v <= ub));

2) __astree_bzero(x, sz);

=> for (int n = 0; n < sz; n++) { *(char*)(x + n) = 0; }

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

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

[Failure Notice #26732]

Problem Description:

——————–

The analyzer fails to report the use of dangling pointers in comparisons that occur in expressions of a certain form.

Scenario:

———

The analyzer fails to report usage of a dangling pointer if the pointer is used in a comparison whose result is used as a scalar value (not directly in a condition).

For example, consider the following if-statements which are controlled by expressions that tests a pointer ‘p’, and assume that ‘p’ may be dangling:

if (p != 0) …       // dangling pointer reported

if ((p !=0) == 1) … // dangling pointer *not* reported

_Bool b = (p!=0);     // dangling pointer *not* reported

Affected versions:

——————

All versions since release 16.10. Previous releases did not report usage of dangling pointers.

Troubleshooting:

—————-

There is no workaround for the issue.

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

2019-06-25T04:34:55+00:00