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

  • Subject: [Frama-c-discuss] [Jessie] FP overflow
  • From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
  • Date: Mon, 4 Nov 2013 15:24:29 -0200
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>