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

Hello, 

>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).

Ok, this is not obvious but it clarifies for me the value behaviour.

But with wp alone I do not understand why 

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

is validated by: 

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

Is this related to oddities in the modeling of float reported on bts
(although -wp-model float is not used in this issue)
https://bts.frama-c.com/view.php?id=2228 
?

Maurice