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.tfind_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-1l..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.bottomconflate_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.tfind ?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 -> tadd_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 -> tThe 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 -> treduce_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 -> tSame 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 -> tFor variables that are coming from the AST, this is equivalent to uninitializing them.
val cardinal_estimate : t -> Cvalue.CardinalEstimate.t