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

I am happy to assume that the inputs to the function are not NaNs (Jessie's default interpretation), so the contract should hold, right?  Then it is just a question of why Z3 can't prove it.  Is there a way to see the actual query that is submitted to Z3 (or any other prover)?

As to Claude's comment that he has seen many VCs that Z3 could not discharge, I have seen this too, but only when using Frama-C+Jessie+Why.   When I have used Z3, CVC3, etc., by hand, it is usually the opposite -- Z3 wins.  Also Z3 wins many competitions.   So it makes me wonder if there is a problem in the way the translation to Z3 is done.  If it is really a shortcoming of Z3, it would be interesting to understand why.

-Steve

On Oct 8, 2013, at 4:16 AM, Guillaume Melquiond <Guillaume.Melquiond at inria.fr> wrote:

> 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
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss