module Eval_exprs:sig
..end
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
Reduction by operators condition
exception Not_an_exact_loc
val not_an_exact_loc : exn
exception Reduce_to_bottom
val reduce_to_bottom : exn
exception Offset_not_based_on_Null of Locations.Zone.t option * Locations.Location_Bytes.t * Cil_types.typ
exception Cannot_find_lv
val cannot_find_lv : exn
exception Too_linear
val too_linear : exn
type
cond = {
|
exp : |
|
positive : |
val do_promotion_c : with_alarms:CilE.warn_mode ->
src_typ:Cil_types.typ ->
dst_typ:Cil_types.typ -> Cvalue.V.t -> Cil_types.exp -> Cvalue.V.t
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
val eval_host : with_alarms:CilE.warn_mode ->
deps:Locations.Zone.t option ->
Cvalue.Model.t ->
Cil_types.lhost ->
Precise_locs.precise_offset ->
Cvalue.Model.t * Locations.Zone.t option * Precise_locs.precise_location_bits
val pass_cast : Cvalue.Model.t -> exn -> Cil_types.typ -> Cil_types.exp -> unit
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 find_lv : with_alarms:CilE.warn_mode ->
Cvalue.Model.t -> Cil_types.exp -> Cil_types.lval
val find_lv_plus_offset : with_alarms:CilE.warn_mode ->
Cvalue.Model.t -> Cil_types.exp -> Cil_types.lval * Ival.t
e
into lval+offset
; where lval
is a Cil
expression, and offset
is an Ival.t, in bytes.val get_influential_vars : Cvalue.Model.t -> Cil_types.exp -> Locations.location list
val reduce_by_valid_loc : positive:bool ->
for_writing:bool ->
Locations.location -> Cil_types.typ -> Cvalue.Model.t -> Cvalue.Model.t
val eval_binop : with_alarms:CilE.warn_mode ->
Cil_types.exp ->
Locations.Zone.t option ->
Cvalue.Model.t -> Cvalue.Model.t * Locations.Zone.t option * Cvalue.V.t
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_expr_with_deps_state_subdiv : 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 reduce_by_accessed_loc : for_writing:bool ->
Cvalue.Model.t ->
Cil_types.lval -> Locations.location -> Cvalue.Model.t * Locations.location
val eval_lval_one_loc : conflate_bottom:bool ->
with_alarms:CilE.warn_mode ->
Locations.Zone.t option ->
Cvalue.Model.t ->
Cil_types.lval ->
Cil_types.typ ->
Locations.location -> Cvalue.Model.t * Locations.Zone.t option * Cvalue.V.t
val eval_lval : conflate_bottom:bool ->
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 eval_lval_and_convert : with_alarms:CilE.warn_mode ->
Locations.Zone.t option ->
Cvalue.Model.t ->
Cil_types.exp * Cil_types.lval ->
Cvalue.Model.t * Locations.Zone.t option * Cvalue.V.t
val reduce_index : with_alarms:CilE.warn_mode ->
Cil_types.exp option ->
Integer.t ->
Cil_types.exp -> Ival.t -> Cvalue.Model.t -> Cvalue.Model.t * Ival.t
array_size
at indexes index
in state
state
. If index causes an out-of-bounds access, emit an informative
alarm, reduce index
, and if possible reduce index_exp
in state
.val eval_offset : with_alarms:CilE.warn_mode ->
reduce_valid_index:Kernel.SafeArrays.t ->
Locations.Zone.t option ->
Cil_types.typ ->
Cvalue.Model.t ->
Cil_types.offset ->
Cvalue.Model.t * Locations.Zone.t option * Precise_locs.precise_offset *
Cil_types.typ
val topify_offset : with_alarms:CilE.warn_mode ->
Locations.Zone.t option ->
Cvalue.Model.t ->
Cvalue.V.t ->
Cil_types.offset -> Locations.Zone.t option * Locations.Location_Bytes.t
val eval_as_exact_loc : with_alarms:CilE.warn_mode ->
?locv:bool ->
Cvalue.Model.t ->
Cil_types.exp -> Locations.location * Cvalue.V.t * Cil_types.typ
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 reduce_rel_from_type : Cil_types.typ -> Eval_op.reduce_rel_int_float
val reduce_by_left_comparison_abstract : Eval_op.reduce_rel_int_float ->
bool ->
Cil_types.exp ->
Cil_types.binop -> Cvalue.V.t -> Cvalue.Model.t -> Cvalue.Model.t
val reduce_by_left_comparison : Eval_op.reduce_rel_int_float ->
bool ->
Cil_types.exp ->
Cil_types.binop -> Cil_types.exp -> Cvalue.Model.t -> Cvalue.Model.t
val reduce_by_comparison : Eval_op.reduce_rel_int_float ->
bool ->
Cil_types.exp ->
Cil_types.binop -> Cil_types.exp -> Cvalue.Model.t -> Cvalue.Model.t
val reduce_by_cond_enumerate : Cvalue.Model.t ->
cond -> Locations.location list -> Cvalue.Model.t
val reduce_by_cond : Cvalue.Model.t -> cond -> Cvalue.Model.t
Reduce_to_bottom
and never returns Cvalue.Model.bottom
Never returns Model.bottom
. Instead, raises Reduce_to_bottom
val compatible_functions : with_alarms:CilE.warn_mode ->
Cil_types.varinfo -> Cil_types.typ -> Cil_types.typ -> bool
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.Model.offsetmap option