--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on April 2013 ---
> > > >> 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. > Really? So what intervals do Cvo_Fqrp, Cvo_Xf[0] and Cvo_Xf[1] evolve in with the initial conditions in your main()? As David said, it would help if you knew what you are trying to prove. You can do it by trial and error, but it would be faster to go straight for the intervals that can really happen. It will be long enough to go straight for the solution. > We believe that the problem is the use of Frama_C_float_interval. There is only one documented method for getting near-optimal results from Frama-C's value analysis. Sometimes the problem is that the property you are trying to establish is out of reach of this single universal method, and that may be the case for your example. But, for now, the problem is not that. The problem is that you have not followed the method to the end yet. >> 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. The property you are trying to establish, if true, is true because of the relation that holds between Cvo_Fqrp, Cvo_Xf[0] and Cvo_Xf[1] at each iteration. You should have already gotten used to the idea that the value analysis was fundamentally a non-relational analysis where relations are represented, when necessary, by separation of abstract states. Option slevel separates abstract states along the execution paths of the program. What do you do next when separating along the execution paths of the program does not provide the precision you are aiming for? How does the square example in section ?Case analysis? of the manual work? How does this tutorial work: http://blog.frama-c.com/index.php?post/2011/06/02/Skein-7 ? How does this tutorial work: http://blog.frama-c.com/index.php?post/2011/03/26/Helping-the-value-analysis-2? How does this tutorial work: http://blog.frama-c.com/index.php?post/2011/02/10/Verifying-numerical-precision-part-2? What do the solutions in these tutorials have in common? -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130405/82534c8b/attachment.html>