--- layout: fc_discuss_archives title: Message 17 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



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>