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] [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                    |