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
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:
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
l..l+loc.size-1
points to V.bottom
everywhere, the value
is bottom
.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
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.
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
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.
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