--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on April 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Value Analysis - iterative function 2



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