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