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: Maurice.Bremond at inria.fr (Maurice Bremond)
  • Date: Wed, 08 Jun 2016 11:58:22 +0200
Hello, 


I do not understand why these ACSL assertions:

int main()
{
  /*@ assert \is_finite((double) (1./0.)); */
  /*@ assert \is_finite((double) (0./0.)); */
}

are validated by:

frama-c -wp -wp-model float t.c


I have a similar question about the following assertion:

#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.
[...]

As for the first assertions, the kernel generated proof obligation may
be validated by:

frama-c -val t.c -wp -wp-model float

I agree with the kernel warning, but not with its "invalidation" by the
value plugin and wp -wp-model float!


Conversely, with -wp-model float, the assertions

 /*@ assert \is_infinite((double) (1./0.)); */
 /*@ assert \is_NaN((double) (0./0.)); */

seem out of reach.


I find this counterintuitive.


Regards,

Maurice Bremond