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] division by zero and wp plugin + float model

  • Subject: [Frama-c-discuss] division by zero and wp plugin + float model
  • From: boris at yakobowski.org (Boris Yakobowski)
  • Date: Mon, 13 Jun 2016 22:56:47 +0200
  • In-reply-to: <87wply4vm8.fsf@inria.fr>
  • References: <87wply4vm8.fsf@inria.fr>
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>