Module Cvalue.Model

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