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

>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