module Model: sig .. end
Memories. They are maps from bases to memory slices
include Lmap_sig
Functions inherited from Lmap_sig interface
Finding values *
val find_unspecified : ?conflate_bottom:bool ->
t -> Locations.location -> bool * Cvalue.V_Or_Uninitialized.t
find_unspecified ~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. The function
also returns true when the read location may be invalid.
val find : ?conflate_bottom:bool -> t -> Locations.location -> bool * Cvalue.V.t
find ?conflate_bottom state loc returns the same value as
find_indeterminate, but removes the indeterminate flags from the
result. The returned boolean indicates only a possibly invalid
location, not indeterminateness.
Writing values into the state
val add_binding : exact:bool -> t -> Locations.location -> Cvalue.V.t -> bool * 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.
The returned boolean indicates that the location may be invalid.
For this function,
v is an initialized value; the function
Cvalue.Model.add_binding_unspecified allows to write a possibly unspecified
value to
state.
val add_unsafe_binding : exact:bool ->
t -> Locations.location -> Cvalue.V_Or_Uninitialized.t -> bool * t
val add_binding_unspecified : exact:bool ->
t -> Locations.location -> Cvalue.V_Or_Uninitialized.t -> bool * t
Reducing the state
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.
val reduce_binding : t -> Locations.location -> Cvalue.V.t -> t
Deprecated.since Magnesium-20151001. Use a combination of
V.narrow
and
Cvalue.Model.reduce_previous_binding to obtain the same result.
reduce_binding state loc v refines the value associated to
loc in
state according to
v, by keeping the values common
to the existing value and
v.
Creating an initial state
Creating an initial state
The functions below can be used to create an initial state to perform
an analysis. In particular, they can write to read-only locations.
val add_initial_binding : t -> Locations.location -> Cvalue.V_Or_Uninitialized.t -> t
val add_new_base : Base.t ->
size:Abstract_interp.Int.t ->
Cvalue.V.t -> size_v:Abstract_interp.Int.t -> t -> t
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