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] 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