--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on April 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Help with the Value Set Analysis



> I would like to know if is possible to see the interval-congruence values
> (VSA) for the variables itself and not just
> for the return statements. I will clarify my point by the log generated
> using frama-c.
>
> [value] ====== VALUES COMPUTED ======
> [value] Values for function teste:
> ????????? a ? {1; 11; }
> [value] Values for function Soma:
> ????????? __retres ? {10; }
> [value] Values for function Subtrai:
> ????????? __retres ? [-10..8],0%2
> [value] Values for function main:
> ????????? a ? {10; }
> ????????? b ? {0; }
> ????????? i ? {10; }
> ????????? soma ? {10; }
> ????????? subtracao ? {8; }
> ????????? __retres ? {1; }
>
> Why is not shown that a and b for instance is coitained in the VSA [0,10].

I believe that you would like to see the union of the variations
domains of a and b for the entire execution of the analyzed program,
whereas the various options available for displaying results all
display the values in one particular program point (these options are
using -val with the batch version of Frama-C, inserting calls to
Frama_C_show_each_ab(a,b); in a program point of interest, or using
the GUI to click on l-values).

The unions you would like to see are not available directly. The
solution is to write a short plug-in to compute them. The plug-in
could iterate on all statements and compute the union of the states
attached to each. Such a plug-in would have to use a CIL visitor to
visit all the statements (perhaps the simplest example of use of a CIL
visitor is in file src/inout/outputs.ml) and for each statement, to
use function Db.Value.get_state to get a state that can be accumulated
thanks to Relation_type.Model.join. A good initial value for the
accumulator would be (!Db.Value.initial_state_only_globals)(), or
Relation_type.Model.bottom, depending on what exactly you are trying
to do.

Pascal