module Model:sig
..end
include Lmap_sig
Lmap_sig
interfaceval 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: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
l..l+loc.size-1
points to V.bottom
everywhere, the value
is bottom
.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
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
.
You usually want to use conflate_bottom=false
, unless your goal
is to test for the the fact that loc
points to something undeterminate.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
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.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
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
.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
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