--- layout: fc_discuss_archives title: Message 3 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



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