--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on April 2013 ---
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