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

[Frama-c-discuss] [Jessie] FP overflow




Le 04/11/2013 18:24, Rovedy Aparecida Busquim e Silva a ?crit :
> Hi,
> 
> We would like to prove that there is not FP overflow in the following
> computations of aux and Fqrp[i]:
> 
>       aux = Ptr[INDEX]->F_Kf * Fqrp[i] - Ptr[INDEX]->F_A2 * Xf[i][0] -
> Ptr[INDEX]->F_A1 * Xf[i][1]; 
> 
>       Fqrp[i] = aux +  Ptr[INDEX]->F_B2 * Xf[i][0] + Ptr[INDEX]->F_B1 *
> Xf[i][1];
> 
> All variables are bounded with requires annotations values, then we
> supposed the aux and Fqrp[i] variables should be bounded too.
> 
> What could we do to avoid FP overflow?

First, identify for which of the operations the absence of overflow is
not proved.

My guess is that you need again the trick with a ghost variable.

ghost tmp = Ptr[INDEX]->F_Kf
//@ assert ...


> The Ptr[INDEX]->F_Kf variable is initialized in another function with a
> DEFINE value (Fkf). 
> 
> We have inserted the following requires annotation to assure the
> initialization. Is that correct?
>   requires \abs(Ptr[INDEX]->F_Kf - FKf) <= BOUND;
> 
> 
> Best regards,
> Nanci, Luciana, Rovedy
> 
> 
> _______________________________________________
> 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                    |