sig
val eval_expr :
with_alarms:CilE.warn_mode ->
Cvalue.Model.t -> Cil_types.exp -> Cvalue.V.t
val eval_expr_with_deps_state :
with_alarms:CilE.warn_mode ->
Locations.Zone.t option ->
Cvalue.Model.t ->
Cil_types.exp ->
Cvalue.Model.t * Locations.Zone.t option * Locations.Location_Bytes.t
val eval_lval :
with_alarms:CilE.warn_mode ->
Locations.Zone.t option ->
Cvalue.Model.t ->
Cil_types.lval ->
Cvalue.Model.t * Locations.Zone.t option * Cvalue.V.t * Cil_types.typ
val lval_to_loc :
with_alarms:CilE.warn_mode ->
Cvalue.Model.t -> Cil_types.lval -> Locations.location
val lval_to_precise_loc :
with_alarms:CilE.warn_mode ->
Cvalue.Model.t -> Cil_types.lval -> Precise_locs.precise_location
val lval_to_loc_state :
with_alarms:CilE.warn_mode ->
Cvalue.Model.t ->
Cil_types.lval -> Cvalue.Model.t * Locations.location * Cil_types.typ
val lval_to_precise_loc_state :
with_alarms:CilE.warn_mode ->
Cvalue.Model.t ->
Cil_types.lval ->
Cvalue.Model.t * Precise_locs.precise_location * Cil_types.typ
val lval_to_loc_deps_state :
with_alarms:CilE.warn_mode ->
deps:Locations.Zone.t option ->
Cvalue.Model.t ->
reduce_valid_index:Kernel.SafeArrays.t ->
Cil_types.lval ->
Cvalue.Model.t * Locations.Zone.t option * Locations.location *
Cil_types.typ
val lval_to_precise_loc_deps_state :
with_alarms:CilE.warn_mode ->
deps:Locations.Zone.t option ->
Cvalue.Model.t ->
reduce_valid_index:Kernel.SafeArrays.t ->
Cil_types.lval ->
Cvalue.Model.t * Locations.Zone.t option *
Precise_locs.precise_location * Cil_types.typ
type cond = { exp : Cil_types.exp; positive : bool; }
exception Reduce_to_bottom
val reduce_by_cond : Cvalue.Model.t -> Eval_exprs.cond -> Cvalue.Model.t
val reduce_by_accessed_loc :
for_writing:bool ->
Cvalue.Model.t ->
Cil_types.lval ->
Locations.location -> Cvalue.Model.t * Locations.location
exception Cannot_find_lv
val find_lv : Cvalue.Model.t -> Cil_types.exp -> Cil_types.lval
val get_influential_vars :
Cvalue.Model.t -> Cil_types.exp -> Locations.location list
val warn_reduce_by_accessed_loc :
with_alarms:CilE.warn_mode ->
for_writing:bool ->
Cvalue.Model.t ->
Locations.location ->
Cil_types.lval -> Cvalue.Model.t * Locations.location
val resolv_func_vinfo :
with_alarms:CilE.warn_mode ->
Locations.Zone.t option ->
Cvalue.Model.t ->
Cil_types.exp -> Kernel_function.Hptset.t * Locations.Zone.t option
val offsetmap_of_lv :
with_alarms:CilE.warn_mode ->
Cvalue.Model.t ->
Cil_types.lval ->
Precise_locs.precise_location * Cvalue.Model.t *
Cvalue.V_Offsetmap.t Bottom.or_bottom
end