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