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] interfacing non-OCaml programs with Frama-C

  • Subject: [Frama-c-discuss] interfacing non-OCaml programs with Frama-C
  • From: Pascal.CUOQ at cea.fr (Pascal Cuoq)
  • Date: Tue, 20 Jan 2009 16:30:00 +0100
  • In-reply-to: <bacfeaa40901200424j11629bf0p776b0d151f6bf13@mail.gmail.com>
  • References: <5EFD4D7AC6265F4D9D3A849CEA9219191AB11D@LAXA.intra.cea.fr> <bacfeaa40811280930r1b6f0e46xad400ebefbdf4646@mail.gmail.com> <5EFD4D7AC6265F4D9D3A849CEA9219191AB120@LAXA.intra.cea.fr> <bacfeaa40901160754h432d2715u5627b90af7080e57@mail.gmail.com> <5EFD4D7AC6265F4D9D3A849CEA9219191AB147@LAXA.intra.cea.fr> <bacfeaa40901200424j11629bf0p776b0d151f6bf13@mail.gmail.com>
>
> What you really want to do (obtaining tuples) is just one step from
> there: in order to get the tuples the way you want them,
> you have to iterate over the states the function that constructs
> the list of values of your variables.
> I think I don't get quite get it, I was thinking that to get t-uples  
> I would have to modify the way I create the offset_map (well  
> actually I'm not quite sure about what an offset_map is),

An offsetmap is the abstract representation for an array of bytes.
If you are writing an abstract interpreter for programs with any kind of
cast, the simplest way to handle it is to consider that every variable
is an array of bytes.
Note that this includes scalar variables (for instance with
the default target architecture, you can cast the address of an
int variable to the address of an array of 4 chars, and everything
will work. Some approximations may happen but the results will
be correct).

So, the most general information you can get from the analyzer
for an l-value you are interested in is an offsetmap, but
if your variable is a scalar one and you are not interested in
the "array of chars" view, you would instead call
Db.Value.access, which return a simpler view of the contents
of your variable, instead of Db.Value.lval_to_offsetmap
which returns the offsetmap.

Note that with the new hook that I am suggesting you use,
you get a data structure that contains the states.
If you want to do something else with each state than
printing it (for which there is a function ready to use)
you have to work a little (using the functions available
in Relations_type.Model). Typically, you may have to
first use the state to convert your l-value to a "location"
(using Db.Value.lval_to_loc_state),
and then use Relations_type.Model.find to get the value
stored at that location in the state.

> but apparently, it's completely otherwise. "iterate over the states  
> the function that constructs the list of values of your variables"  
> I've read this hundreds of time, but I really don't get it :-/ is  
> there an example somewhere in frama-c's code ?

In the example in my last message, the part

State_set.iter (fun state -> X) superposition

means to iterate over the states contained
in variable superposition (of type State_set.t)
the function that does X, that is, to do X
in sequence over each state contained in
superposition.

In my example, X is to pretty-print the state,
but this is where you could be building a tuple
from the state and adding it to some structure
of yours.

> > I know that (List.length vars_list) will be limited by  
> SemanticUnrollingLevel
> Actually, it won't. What will be limited will be the number of tuples
> you can get this way. (List.length vars_list) is the size of each  
> tuple,
> and you can make it as big as you want.
> So the higher SemanticUnrollingLevel is, the more precise the set of  
> tuples will be ?

Well, yes, but within some limits!
Grouping states together causes approximations (as you have
noticed when at first you were accessing a single state that was
the union of all analysis states). Passing a higher value to option - 
slevel
postpones the time when it becomes necessary to group states together,
and therefore increases precision,
but when the analyzer ceases to group any states at all, you won't
gain any more precision by increasing SemanticUnrollingLevel.

Pascal