--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on April 2010 ---
> 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