--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on January 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Value Analysis plugin versus Simulation Tool



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>