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

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:

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