--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on June 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] division by zero and wp plugin + float model



Hi Maurice,

On Wed, Jun 8, 2016 at 11:58 AM, Maurice Bremond <Maurice.Bremond at inria.fr>
wrote:

>
> #include <__fc_builtin.h>
> int main()
> {
>   double x = Frama_C_double_interval(-1e0, 1e0);
>
>   double x0 = 1/x;
>   /*@ assert \is_finite((double) x0); */
>
> }
>
> The assertion is validated by the value plugin whereas a message coming
> from
> the kernel warns about what seems to be a contrary fact:
>
> frama-c -val t.c
>
> [...]
> t.c:6:[kernel] warning: non-finite double value. assert
> \is_finite((double)((double)1/x));
> t.c:7:[value] assertion got status valid.
> [...]
>
>
Value assumes/proves that the program does not produce NaN or infinite
values during its execution. See for example the Aluminium manual, section
3.2. Thus, as soon as an operation may produce an infinite or a NaN, an
alarm is emitted to exclude this case. In your example, the division may
produce an infinite, and an alarm is generated. This guard exactly
guarantees that x0 contains a finite floating-point value. Afterwards,
Value is free to use this fact, and it can emit a Valid status on your
assertion \is_finite((double) x0).

This is indeed a deviation from the ACSL specification, in which x0 may
contain NaN and infinite values. The semantics implemented by Value is
stricter, and may be too restrictive in some cases. However, it remains
compatible with ACSL, in the sense that a Value-emitted Valid status is
Valid in ACSL *provided that no other alarm has been emitted before in the
trace*. In this case, the alarm \is_finite((double)((double)1/x)) is indeed
emitted before your assertion. And it is unprovable for the values that
would make \is_finite((double) x0) invalid, so all is well!

Two final points:
- in the next release of Frama-C, the alarm will be emitted by Value
itself. The previous labeling [kernel] was historical and misleading
- having an user-activated mode that handles NaNs and infinite values is
high on our TODO list

HTH,

-- 
Boris
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160613/f188920f/attachment.html>