module Model: sig
.. end
Memories. They are maps from bases to memory slices
include Lmap_sig
Functions inherited from Lmap_sig
interface
include Lattice_type.With_Narrow
Finding values *
val find_indeterminate : ?conflate_bottom:bool ->
t -> Locations.location -> Cvalue.V_Or_Uninitialized.t
find_indeterminate ~conflate_bottom state loc
returns the value
and flags associated to
loc
in
state
. The flags are the union
of the flags at all the locations and offsets corresponding to
loc
.
The value is the join of all the values pointed by
l..l+loc.size-1
for all
l
among the locations in
loc
. For an individual
l
,
the value pointed to is determined as such:
- if no part of
l..l+loc.size-1
is V.bottom
, the value is the most
precise value of V
approximating the sequence of bits present at
l..l+loc.size-1
- if
l..l+loc.size-1
points to V.bottom
everywhere, the value
is bottom
.
- if
conflate_bottom
is true
and at least one bit pointed to by
l..l+loc.size-1
is V.bottom
, the value is V.bottom
- if
conflate_bottom
is false
and at least one bit pointed to by
l..l+loc.size-1
is not V.bottom
, the value is an approximation
of the join of all the bits at l..l+loc.size-1
.
As a rule of thumb, you must set conflate_bottom=true
when the
operation you abstract really accesses loc.size
bits, and when
undeterminate values are an error. This is typically the case when
reading a scalar value. Conversely, if you are reading many bits at
once (for example, to approximate the entire contents of a struct),
set conflate_bottom
to false
-- to account for the possibility
of padding bits. The default value is true
.
val find : ?conflate_bottom:bool -> t -> Locations.location -> Cvalue.V.t
find ?conflate_bottom state loc
returns the same value as
find_indeterminate
, but removes the indeterminate flags from the
result.
Writing values into the state
val add_binding : exact:bool -> t -> Locations.location -> Cvalue.V.t -> t
add_binding state loc v
simulates the effect of writing
v
at location
loc
in
state
. If
loc
is not writable,
bottom
is returned.
For this function,
v
is an initialized value; the function
Cvalue.Model.add_indeterminate_binding
allows to write a possibly indeterminate
value to
state
.
val add_indeterminate_binding : exact:bool -> t -> Locations.location -> Cvalue.V_Or_Uninitialized.t -> t
Reducing the state
The functions below can be used to refine the value bound to a given
location. In both cases, the location must be exact.
val reduce_previous_binding : t -> Locations.location -> Cvalue.V.t -> t
reduce_previous_binding state loc v
reduces the value associated to loc
in state; use with caution, as the inclusion between the new and the
old value is not checked.
val reduce_indeterminate_binding : t -> Locations.location -> Cvalue.V_Or_Uninitialized.t -> t
Same behavior as reduce_previous_binding
, but takes a value
with 'undefined' and 'escaping addresses' flags.
Misc
val uninitialize_blocks_locals : Cil_types.block list -> t -> t
val remove_variables : Cil_types.varinfo list -> t -> t
For variables that are coming from the AST, this is equivalent to
uninitializing them.
val cardinal_estimate : t -> Cvalue.CardinalEstimate.t