--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on October 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] z3 failure




Pascal, I am sure you know that the default model in Jessie rules out
special values (infinities and NaNs). This means two things:

* for any FP operation it must be proved that no overflow occur (or
equivalently that the result is not NaN nor infinity)

* consequently, we can assumed safely that input FP data of any function
is non-special. This is the case of the example given.

I strongly believe this is the best model for 99.9% of programs, i.e
except in very particular cases, special values should never show up in
a program.

- Claude

PS: just for the braves who want to play with special values, Jessie has
a model with special values

#pragma JessieFloatModel(full)

Le 07/10/2013 01:27, Pascal Cuoq a ?crit :
> Do you expect the property to be provable or not? The program below
> shows that it does not hold for typical C implementations with IEEE 754
> representations for floating-point types:
> 
> $ cat d.c
> #include <stdio.h>
> 
> double a = 0. / 0.;
> 
> int main(){
>   double b = a;
>   printf("%d\n", a == b);
> }
> $ gcc d.c && ./a.out 
> 0
> 
> It would be considered a bug in Jessie if it generates, for the same
> program property, a provable obligation for some provers and an
> unprovable one for others. I would just like it to be clear whether,
> with Jessie's default models regarding aliasing and floating-point, we
> are looking for an issue with the Z3 output or with Alt-Ergo, CVC3, and
> CVC4's.
> 
> 
> 
> _______________________________________________
> 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                    |