Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Value Analysis plugin versus Simulation Tool
  • From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
  • Date: Mon, 28 Jan 2013 16:14:23 -0300
  • In-reply-to: <CAOH62Ji-98BYUQ=wfpUrc8YO9AyssPn8Hnw-XNLzM556a7g15A@mail.gmail.com>
  • References: <CAEtoXR1A-_NAuDiY+PAG6ds6Z3PqOh6NrE1GdLDSt7LM2HcTnA@mail.gmail.com> <CAOH62Ji-98BYUQ=wfpUrc8YO9AyssPn8Hnw-XNLzM556a7g15A@mail.gmail.com>
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>