--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on June 2016 ---
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