Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Floating-point NaN Detection

Hello,

> I am testing if frama-c can detect NaN. Here is my test code.

Well, as the manual says (pages 16-17), there are two circumstances
where NaN and infinites are detected and excluded:

A - the result of a floating-point operation ;
B - a value from memory that is not already known to be a finite
floating-point number is used as an argument to a floating-point
operation.

Your code does neither: passing *p as an argument to the function
printf, which in this case expect a double as fourth argument, is not
a floating-point operation. Generally speaking the value analysis
tries to avoid emitting alarms for operations that amount to copying a
slice of memory from a place to another because that produces annoying
false alarms -- see for instance the explanation for dangling
addresses and uninitialized variables also page 17 of the value
analysis manual.

I changed your program a little to illustrate this:

#define NULL ((void*)0)

void NaN(int c[])
{
       double * p = NULL;
       double d1, d2, d3;
       p = c;
       d1 = *p; /* line 8 */
       d2 = *p + 1; /* line 9 */
       d3 = 0. / *p; /* line 10 */
       printf("integer c[0] = %u, c[1] = %d --> double %f\n", c[0], c[1], *p);
}

int main(int argc, char * argv[])
{
       int c[2] = {argc, argc};
       NaN(c);
       return 0;
}

Commandline: frama-c -val t.c

Results:

t.c:9:[value] warning: float value must be finite: assert(TODO)

-> type B floating-point alarm. No type A alarm for line 9 because in
round-to-nearest there cannot be an overflow with that operation as
long as the argument is already assumed to be finite.

...
t.c:10:[value] warning: converting value to float: assert(TODO)

-> type B floating-point alarm again. For some reason there are
several messages for the same warning. The messages will be unified in
the next version.

t.c:10:[value] warning: float division: assert(TODO)

-> Please ignore this message. It doesn't make sense to check
specifically for division by zero when there is a perfectly good
mechanism applied to all floating-point operations that checks if the
result is infinite or NULL. This warning is left over from a time when
the floating-point implementation in the value analysis was more
rudimentary, and will be removed in the next version.

t.c:10:[kernel] warning: float operation: assert \is_finite("/", 0., *p);

-> This message is a type A floating-point alarm and tries to give you
information about which operation may overflow or produce NaN,
although the syntax of the produced ACSL predicate will again change
in the next version since floating-point representations have now been
integrated there.

You didn't get a warning for line 8, but line 8 didn't use an unknown
value in a floating-point operation. Consistently with this, at the
end of the program d1 is only known to be [--..--], a completely
unknown bit pattern that contains NaN and infinites. If you used d1 as
argument in a floating-point operation, then you would get a warning.

> By the way, I also test infinite value. It works fine.

All the same warnings apply to both unwanted infinites and unwanted
NaNs. There is no distinction between them.

Pascal