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: dmentre at linux-france.org (David MENTRE)
  • Date: Wed, 3 Apr 2013 09:22:36 +0200
  • In-reply-to: <CAEtoXR01v6q7g6Gv2zsvGpmR3w786YKP2HntVvdS4KTSFzaOog@mail.gmail.com>
  • References: <CAEtoXR01v6q7g6Gv2zsvGpmR3w786YKP2HntVvdS4KTSFzaOog@mail.gmail.com>
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