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_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
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
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