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

  • Subject: [Frama-c-discuss] z3 failure
  • From: Claude.Marche at inria.fr (Claude Marché)
  • Date: Mon, 07 Oct 2013 09:10:54 +0200
  • In-reply-to: <CAOH62JjsXkn6GU9Y=HcQ-N+_ZyG=N9BL0=5vOL==tSthz4T-8w@mail.gmail.com>
  • References: <E33ED61C-4FD1-410D-B327-7C4D744351D2@udel.edu> <CAOH62JjsXkn6GU9Y=HcQ-N+_ZyG=N9BL0=5vOL==tSthz4T-8w@mail.gmail.com>

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                    |