--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on November 2013 ---
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? 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 -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131104/76973b89/attachment.html> -------------- next part -------------- A non-text attachment was scrubbed... Name: site008c_43.c Type: text/x-csrc Size: 1682 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131104/76973b89/attachment.c>