--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on May 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-c-discuss Digest, Vol 36, Issue 6



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