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