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 : Cvalue.Model.t -> Cil_types.exp -> Cil_types.lval
val find_lv_plus_offset : 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 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 : 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 : 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 warn_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 : ?locv:bool ->
Cvalue.Model.t ->
Cil_types.exp -> Locations.location * Cvalue.V.t * Cil_types.typ
locv
to true
if you want to compute the value pointed to by
loc
simultaneously.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 warn_reduce_shift_rhs : with_alarms:CilE.warn_mode ->
Cvalue.Model.t ->
Cil_types.typ ->
Cil_types.exp ->
Locations.Location_Bytes.t -> Cvalue.Model.t * Locations.Location_Bytes.t
size
bits.
Also reduce the state when possibleval warn_reduce_shift_left : with_alarms:CilE.warn_mode ->
Cvalue.Model.t ->
Cil_types.typ ->
Cil_types.exp ->
Locations.Location_Bytes.t ->
Cil_types.exp ->
Locations.Location_Bytes.t ->
Cvalue.Model.t * Locations.Location_Bytes.t * Locations.Location_Bytes.t
val reduce_previous_value : Cvalue.Model.t -> Cil_types.exp -> Cvalue.V.t -> Cvalue.Model.t
val reduce_by_left_comparison_abstract : bool ->
Cil_types.exp ->
Cil_types.binop -> Cvalue.V.t -> Cvalue.Model.t -> Cvalue.Model.t
val reduce_by_left_comparison : bool ->
Cil_types.exp ->
Cil_types.binop -> Cil_types.exp -> Cvalue.Model.t -> Cvalue.Model.t
val reduce_by_comparison : 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_modulo : Cvalue.Model.t ->
cond ->
Cil_types.exp ->
Cil_types.exp -> Cil_types.binop -> Cil_types.exp -> Cvalue.Model.t
state cond eqop exp1lv exp1mod exp2
reduces state
by the property
exp1lv mod exp1mod =!= exp2
, =!=
being the conjunct of eqop
(which
must be either ==
or !=
) and cond.positive
. Currently, only the
location pointed to by exp1lv
(if any) is reduced, and only when exp1mod
and exp2
are constants.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.V_Offsetmap.t_top_bottom
Int_Base.Error_Top