module Eval_exprs:sig
..end
Detects if an expression can be considered as a lvalue even though it is
hidden by a cast that does not change the lvalue. Raises exn
if it cannot.
TODO: When the goal is to recognize the form (cast)l-value == expr,
it would be better and more powerful to have chains of inverse functions
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 : |
|
positive : |
exception Reduce_to_bottom
val reduce_by_cond : Cvalue.Model.t -> cond -> Cvalue.Model.t
Model.bottom
. Instead, raises Reduce_to_bottom
raises Reduce_to_bottom
and never returns Cvalue.Model.bottom
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_top_bottom
Int_Base.Error_Top