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