Previous  Up  

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 : with_alarms:CilE.warn_mode ->
       conflate_bottom:bool ->
       t -> Locations.location -> 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 : with_alarms:CilE.warn_mode ->
       conflate_bottom:bool -> t -> Locations.location -> Cvalue.V.t
find ~with_alarms state loc returns the same value as find_indeterminate, but removes the flags from the result. If either the "unitialized" or "escaping" address flag was present, the corresponding alarm is raised by the function.
val find_and_reduce_indeterminate : with_alarms:CilE.warn_mode -> t -> Locations.location -> t * Cvalue.V.t
Similar to find, but we expect a non-indeterminate result; if the value returned had escaping or uninitialized flags, they are removed in the state that is returned along with the cvalue.

Writing values into the state


val add_binding : with_alarms:CilE.warn_mode ->
       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_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 -> 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_binding : t -> Locations.location -> Cvalue.V.t -> t
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 reduce_by_initialized_defined_loc : (Cvalue.V_Or_Uninitialized.t -> Cvalue.V_Or_Uninitialized.t) ->
       Locations.Location_Bits.t -> Abstract_interp.Int.t -> t -> t
val uninitialize_blocks_locals : Cil_types.block list -> t -> t
val uninitialize_formals_locals : Cil_types.fundec -> t -> t