Module Eval_exprs

module Eval_exprs: sig .. end
Reduction by operators condition

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

Reduction by operators condition
type cond = {
   exp : Cil_types.exp;
   positive : bool;
}
exception Reduce_to_bottom
val reduce_by_cond : Cvalue.Model.t -> cond -> Cvalue.Model.t
Never returns Model.bottom. Instead, raises Reduce_to_bottom

Reduction by accesses
val reduce_by_accessed_loc : for_writing:bool ->
Cvalue.Model.t ->
Cil_types.lval -> Locations.location -> Cvalue.Model.t * Locations.location

Misc functions related to reduction
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
May raise Int_Base.Error_Top