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] full IEEE754 model in Jessie


Yes Pascal, in ACSL, "==" on floats is equality of the reals they
denote. The predicate corresponding to IEEE754 equality is "\eq_float"
(ACSL manual page 23)

With the following file

---------->8------------
#pragma JessieFloatModel(full)

int main(){
  double a = 0. / 0.;

  //@ assert \is_NaN(a);
  double b = a;
  //@ assert \is_NaN(b);
  //@ assert a == b;
  //@ assert \eq_float(a,b);
}
---------->8------------

Jessie can prove the 3 first assertions by not the last one. Seems
perfectly correct to me.

- Claude

Le 07/10/2013 22:35, Pascal Cuoq a ?crit :
> On Mon, Oct 7, 2013 at 9:10 AM, Claude March? <Claude.Marche at inria.fr
> <mailto: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
> 
> 
> 
> _______________________________________________
> 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
> 

-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           |
Universit? Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |