--- layout: fc_discuss_archives title: Message 26 from Frama-C-discuss on November 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Value Analysis - assertion, slevel and sqrt function



Hi Pascal,

Thanks for your explanation.
In fact, with Frama_C_dump_each()  is easier to see what  happens.

Now, we will apply this in our case study, that is much more complex.

Thanks a lot!

Best regards,
Rovedy/Nanci/Luciana



2012/11/22 Pascal Cuoq <pascal.cuoq at gmail.com>

>
> > It has worked with the minimum value equal 32:
> > >> frama-c -val sqrt.c /usr/share/frama-c/builtin.c
> /usr/share/frama-c/math.c -slevel 32
>
> Your annotations, with their 6 disjunctions, define 2^6 (64) cases. 64 is
> therefore the minimal value of -slevel that will certainly make the
> analysis work. If you use less, it may work or not depending on the
> propagation order (which is inscrutable). It may work and then cease to
> work because of the slightest change in the program, such as one
> additional, unrelated statement. Conclusion: for this example, use 64 (or
> more).
>
> > 2- the program called the function Frama_C_show_each to verify the value
> of the variables, but we have observed that the function is called several
> times. Why does it occur?
>
> Before the first assertion, there is one abstract state being propagated.
> The first assertion splits it in two. The second assertion splits each of
> these in two (there are now 4 abstract states). And so on until there are
> 64 at the end of the function, where they are finally gathered.
>
> Frama_C_show_each_aa(aux); prints the value of aux in each of the 8 (if I
> count correctly) states already separated at that point. The values for aux
> is the same in some of these 8 states, so you may see several times the
> same line.
>
> If you want to see the propagation process more clearly, replace one or
> several  Frama_C_show_each_? with Frama_C_dump_each();
> This will allow you to see the complete states, and it will be clear why
> they are different although they have the same values for aux.
>
>
>
> _______________________________________________
> 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/20121124/a5ee3798/attachment.html>