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

  • Subject: [Frama-c-discuss] Accessing results of the value analysis for arrays/structs
  • From: Pierre.Karpman at rennes.supelec.fr (Pierre Karpman)
  • Date: Tue, 28 Feb 2012 13:47:05 +0100
Hello,

I'm currently writing some code that's using results from the value 
analysis plugin, and I have troubles accessing the computed values for 
arrays and structures.

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

I also have some troubles 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.

So my questions are:
-is this information about the location of the stuff in the offsetmap 
really lost when folding/iterating, or is there an API to access it 
(maybe thanks to a standard Cvalue.V function that I overlooked)?
- if not, what's the best way to go through an offsetmap while still 
being able to determine the value of a single 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?

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?

Regards,
Pierre

P.S.
Don't hesitate to ask for more details about how the whole 
folding-on-offsetmaps-function works, if you think it's relevant. 
Basically it's the nesting of:
Cvalue.Model.fold_base_offsetmap
Cvalue.V_Offsetmap.fold
Locations.Location_Bytes.fold_i (don't think at all this one's involved 
in the matter; my problem's occurring before it's called).