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] Frama-c-discuss Digest, Vol 36, Issue 6

  • Subject: [Frama-c-discuss] Frama-c-discuss Digest, Vol 36, Issue 6
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Tue, 10 May 2011 18:13:18 +0200
  • In-reply-to: <BANLkTikKC_QMe=a8uJG0hAbx6z1WN8wSPg@mail.gmail.com>
  • References: <mailman.55.1304762445.16842.frama-c-discuss@lists.gforge.inria.fr> <BANLkTikKC_QMe=a8uJG0hAbx6z1WN8wSPg@mail.gmail.com>
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