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] z3 failure

On 07/10/2013 22:35, Pascal Cuoq wrote:

> So what happens with the ACSL formula a == b, when the program
> variable b contains a copy of the program variable a (that contain NaN),
> in this ?full? float model, then?
>
> Because == is still the (reflexive) mathematical equality, not the
> IEEE equality between doubles that can also be introduced in ACSL
> as a convenient additional predicate ieee754_eq of double arguments
> that would match the semantics of == in C, right?
>
> And, incidentally, a==b is typed as an equality between reals
> in this case, isn't it? So the formula is in a way equivalent to:
> (real)NaN == (real)NaN
> And the above formula is not dissimilar to 1 / 0 == 1 / 0, in
> that neither side can be evaluated further (but ACSL, as
> a first-order logic, is total, so these terms exist).
>
> And, like 1/0 == 1/0, it is an instance of \forall x, x == x,
> so it is correct for a prover to infer that this formula is true?

I am not able to test it in practice, so I will give the theoretical answer.

A prover will be able to prove the formula, as long as your two NaNs 
come from the exact same place. So, in your example where b is truly a 
copy of a, then a == b will hold. Otherwise, the non-determinism that 
occurs while creating NaN data will cause the equality to fail.

Best regards,

Guillaume