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 Mon, Oct 7, 2013 at 9:10 AM, Claude March? <Claude.Marche at inria.fr>wrote:

>
> Pascal, I am sure you know that the default model in Jessie rules out
> special values (infinities and NaNs).


Ahem. Yes, of course, I know the large and the small of it.
But for the sake of everyone else on this list, please explain it
as if I wasn't such an expert.


> PS: just for the braves who want to play with special values, Jessie has
> a model with special values
>
> #pragma JessieFloatModel(full)
>

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?

Pascal
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131007/bc4bc509/attachment.html>