--- layout: fc_discuss_archives title: Message 10 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



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