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] Accessing results of the value analysis for arrays/structs

Hello,

>
> One alternative way to get the value at arr[4] would be to build a
> representation for the lvalue "arr[4]", translate that representation
> of an lvalue to a location, and pass this location to, say, function
> Cvalue.Model.find.
This looks like the most relevant way for me to do things, as I don't 
even have to build the lvalues (the code I'm using already knows the 
"arr[4]" and the likes as such).
I'm in the way of checking for (potential) bugs, but right know I have a 
small function that works quite fine by doing it this way.

> >/     I guess that an easy answer would be "by doing like the offsetmap printing function", but this one seems to access the offsetmap "from inside", and I'm not sure yet that it'd be possible to emulate it?
> /
> Just to reassure you, the printing function doesn't have any
> information that Cvalue.V_offsetmap.fold does not reveal.

OK. I don't think I'll have to use fold now (the solution from above 
seems better), but I'll keep this in mind if I ever need to.

> >/  and concerning the structures
> />/
> />/  -how is it possible to map an Lvalue representing an access to a structure (e.g. struct.field1.field2) to an offset in the offsetmap, or to its value, as computed by the value analysis plugin?
> /
> That would be function lval_to_loc_state. I'm not sure it is visible.
It seems like I don't have to do anything specific to deal with 
structures now; they fit pretty much in what the function I wrote about 
above can do ; lval_to_loc_state looks pretty much usable, and I'm using 
it in this function.

Thanks a lot for your answers,
Pierre
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120229/b70c4d3d/attachment.htm>