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,

> My first problem is that when folding a function through Cvalue.V_Offsetmap (or iterating through Cvalue.V_Offsetmap.iter_contents), I can't manage to get the information about the location of the resulting values. That is, if I have an offsetmap which when pretty-printed looks like:
> [rbits 0 to 31] ? {5}
> [rbits 32 to 63] ? {1}
> [rbits 64 to 95] ? {10}
> [rbits 96 to 159] ? {0}
> [rbits 160 to 191] ? UNINITIALIZED;
> when I'm (say) folding on it, I only manage to get the list (5, 1, 10, 0, UNINIT.) (when seeing it as a list of Cvalue.V_Or_Uninitialized), losing the information about the location/offset range of those values.


You probably want to use function fold for that.

? val fold : (Int.t * Int.t -> Int.t * Int.t * y -> 'a -> 'a) -> t -> 'a -> 'a

Your function will get the location of each binding in the offsetmap
as the first pair argument, and some alignment information in the
triple that's a pain to explain. But then again...

>
> I'm quite annoyed with that because I'd like to be able to get the value of single fields (directly) from the offsetmap (e.g. if the previous example were from a 1D-int32-array "arr", I'd like to be able to map, say arr[4], to 0).


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.

> I also have some trouble mapping the field of a structure to its corresponding offset
> in the?offsetmap. I first thought about using the "foffset_in_bits" field from the
> Cil "fieldinfo" structure, but it seems that this one's never initialized.

Use bitsOffset typ (Field(fi,NoOffset)) with typ the type of the
struct and fi the field.

> ? 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.

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