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] Value Analysis - iterative function 2

  • Subject: [Frama-c-discuss] Value Analysis - iterative function 2
  • From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
  • Date: Thu, 4 Apr 2013 09:41:33 -0300
  • In-reply-to: <CAC3Lx=bG7F=P4uMsbQXW6W0brhyk6KSiT=Sh4WhsdV0jwny0hA@mail.gmail.com>
  • References: <CAEtoXR01v6q7g6Gv2zsvGpmR3w786YKP2HntVvdS4KTSFzaOog@mail.gmail.com> <CAC3Lx=bG7F=P4uMsbQXW6W0brhyk6KSiT=Sh4WhsdV0jwny0hA@mail.gmail.com>
Hello David,

Thank you.

>> Do you have a pencil & paper analysis that proves that such behaviour
>> should not occur? Is your algorithm numerically stable?

This function is part from aerospace control software and it works well.
We have tested the function in a isolated way with a input array and it
works well also.
We believe that the problem is the use of Frama_C_float_interval.

>> I would try to increase -slevel, to 10000 or even 100000.

We have increased the -slevel to 10000 and 100000.
It did not work, there was a overflow.

>> Frama-C like any other formal analysis tool is not a magic tool. You
>> should guide it based on your knowledge of the code you are analysing.

Anyway, we will carefully analyze the function again.

Thank you!
Best regards.
Rovedy, Luciana, Nanci










2013/4/3 David MENTRE <dmentre at linux-france.org>

> Hello,
>
> I probably have not more knowledge than you. Anyway, here are some
> comments.
>
> 2013/3/26 Rovedy Aparecida Busquim e Silva <rovedy at ig.com.br>:
> > The filter algorithm is implemented as a iterative process whose next
> > iteration is calculated based on the previous calculated value. In that
> > process, the successive calculations with the Cvo_Xf and Cvo_Fqrp
> variables
> > imply accumulated values that grow until reaching the maximum value of
> the
> > double variable.
>
> Do you have a pencil & paper analysis that proves that such behaviour
> should not occur? Is your algorithm numerically stable?
>
> > Is there an annotation or a command line option to deal with this type of
> > iterative algorithm?
>
> As far as I know, there is no such magic flag.
>
> I would try to increase -slevel, to 10000 or even 100000.
>
> Frama-C like any other formal analysis tool is not a magic tool. You
> should guide it based on your knowledge of the code you are analysing.
>
> Good luck!
> Best regards,
> david
>
> _______________________________________________
> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130404/180d0e01/attachment.html>