--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on January 2013 ---
Hi Pascal, Thanks a lot for your answer. We will read the blog and the paper about this topic. Best regards, Rovedy, Luciana e Nanci 2013/1/25 Pascal Cuoq <pascal.cuoq at gmail.com> > Hello, > > On Fri, Jan 25, 2013 at 2:41 PM, Rovedy Aparecida Busquim e Silva > <rovedy at ig.com.br> wrote: > > The first scenario considered the maximum range of values accepted by the > > sensors (Frama C float interval and Frama C interval functions). The > > analysis was performed smoothly and gave valid ranges of values for the > > variables. > > This is a valid and often useful method for using the value analysis. > > > In the second scenario it was adopted a different approach. It was used > all > > the values of sensors measurements obtained from a flight simulation > record > > (ascii file) as input to the Value Analysis/Frama-, i. e., the Frama C > > interval functions do not were used. As a result, the analysis gave > > variables profiles very similar to the simulation ones. > > > > Is valid the second scenario? Can the Value Analysis/Frama-C be used as a > > tool for simulation? > > This method is also valid and useful. When the inputs are precisely known, > for instance when they come from a reference dataset, the value > analysis can be used as a C interpreter simply by passing a large > argument to option -slevel. > > The advantage is analysis precision: if the analysis remains deterministic > until the end, then there are no false alarms. In other words, any alarm > corresponds to a real problem. When you are used to studying > alarms obtained with the first method, this is very comfortable. > > Compared to execution, the advantage is that interpreting C with > the value analysis allows detecting undefined behaviors that cannot > be detected by testing, even with assistance from popular tools such > as Valgrind. > > One reason Frama-C's value analysis works so well as a C > interpreter is that we specifically worked on this aspect in order > to fix bugs in it that also affected its use as a static analyzer. > The research article is linked from: > > http://blog.frama-c.com/index.php?pages/Csmith-testing > > Additional information that did not fit in the article is provided > on the page. > > Regards, > > Pascal > > _______________________________________________ > 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/20130128/3162f053/attachment.html>