--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on January 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] interfacing non-OCaml programs with Frama-C



Hi,

I kept playing with frama-c's source code and now it's a bit easier for me
to do what I have in mind, however I still haven't really figured out how to
use the slevel option from the value analyzis plugin.

For now, this is how I retrieve the variation domain of a list of variables
at a particular instruction in the project (I'm not sure it's the proper way
to do it).

for i = 0 to ((List.length vars_list) - 1) do
  match (List.nth vars_list i) with
  | Lval(lv) ->
    let offsetmap_b = !Db.Value.lval_to_offsetmap
~with_alarms:CilE.warn_none_mode ki lv in
    Format.printf "%s" (fprintf_to_string "'%a'" (self#pretty_offsetmap lv)
offsetmap_b);
  | _ ->

(pretty_offsetmap being ripped off from value/register_gui.ml, ki being the
current stmt in the visitor)

Now, I would like to retrieve as for the variation domain of this list,
still at a particular instruction in the project, a set of t-uples, does
someone have any hint on how to do this ? I know that (List.length
vars_list) will be limited by SemanticUnrollingLevel, but couldn't find in
the source code how to ask for that.

Regards

On Mon, Dec 1, 2008 at 5:01 PM, CUOQ Pascal <Pascal.CUOQ at cea.fr> wrote:

> If what you are really interested in is a set of tuples of possible values
> for the variables of the program, you can have this with the -slevel
> option of the value analysis. But note that when the value analysis
> gives you the set {(0,1,1),(1,0,1)}, it neither guarantees that there
> are at least two different paths (one of the tuples could correspond
> to a path that is in fact not feasible at all), nor that there are at most
> two different paths. On the following example
>
> if (complex condition)
> {
>  y =1
>  x = 2;
> }
> else
> {
>  x = 2;
>  y = 1;
> }
>
> the analyzer will provide the (2,1) tuple for (x,y) only once, although
> this value can be obtained through two different paths. This is
> because the analyzer systematically checks if a tuple (say, the tuple
> coming
> from the else branch) is included in the tuples it already has
> (the tuple for the then branch). This inclusion check is also how
> the analyzer may give correct results for a loop
> that takes 1000 iterations at run time
> (or even a loop that does not obviously terminate)
> without running through the body of the loop 1000 times.
>
> The guarantee is that each possible path at run-time gives a
> (so-called "concrete") tuple of values
> that is included in at least one of the "abstract" tuples
> computed by the analyzer.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090116/7d140a3a/attachment.htm