--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on May 2011 ---
If you subscribed to the mailing list digest, then you MUST edit the subject when replying, and quote only a few relevant lines you are replying to. > At a glance, we get some results which type is Cvalue_type.V and that > encodes ranges > of values, however we have no clue about how to get the information that > follow : > > -> Gettng the infimum and the supremum bounds of this range of values. > -> Getting the set of the elements whenever it is possible. Cvalue_type.V is a module. You mean Cvalue_type.V.t, which is a type. And what are the infimum and supremum bounds of {{ &a; &b; }} or, for that matter, {{ &a; &NULL + {123456}; }} ? Your problem seems to be that you are not familiar enough with OCaml to write your own plug-in. You have to realize that you are in the same situation than if you were asking for help with C on the linux-kernel mailing list. Nevertheless, the module Cvalue_type.V includes the module Locations.Location_Bytes which is described in memory_state/locations.mli between the lines module Location_Bytes : sig and the first end that follows. The type t of that module has the constructors | Top of Top_Param.t * Origin.t | Map of M.t I expect that you have only the Map case in your examples. The Map constructor embed a value of type M.t which is a map from bases (type Base.t) to sets of integers (type Ival.t), that happens to be implemented as a Patricia tree (but you do not need to know that because only a few functions are provided to manipulate objects of type M.t). In module Cvalue_type.V, you can find additional helper functions, such as one named project_ival that directly converts a value of type Cvalue_type.V.t to Ival.t if possible. Pascal