module Eval_stmt: sig
.. end
Value analysis of statements and functions bodies
val compute_call_ref : (Kernel_function.Hptset.elt ->
call_kinstr:Cil_types.kinstr ->
Cvalue.Model.t ->
(Cil_types.exp * Cvalue.V_Offsetmap.t) list -> Value_types.call_result)
Pervasives.ref
val need_cast : Cil_types.typ -> Cil_types.typ -> bool
val do_assign_abstract_value : with_alarms:CilE.warn_mode ->
Cvalue.Model.t ->
Cil_types.typ -> Locations.location -> Cvalue.V.t -> Cvalue.Model.t
Precondition: the type of v
and the type of loc_lv
may be different
only through a truncation or an extension.
This function will not perform any conversion (float->int, int->float, ...)
exp
should not be bottom (for optimization purposes in the caller).
exception Do_assign_imprecise_copy
val do_assign_one_loc : with_alarms:CilE.warn_mode ->
Locals_scoping.clobbered_set ->
warn_indeterminate:bool ->
Cvalue.Model.t ->
Cil_types.lval ->
bool ->
Cil_types.typ -> Cil_types.exp -> Locations.location -> Cvalue.Model.t * bool
val do_assign : with_alarms:CilE.warn_mode ->
Kernel_function.t ->
Locals_scoping.clobbered_set ->
Cvalue.Model.t -> Cil_types.lval -> Cil_types.exp -> Cvalue.Model.t
exception Too_linear
val do_assign : with_alarms:CilE.warn_mode ->
Kernel_function.t ->
Locals_scoping.clobbered_set ->
Cvalue.Model.t -> Cil_types.lval -> Cil_types.exp -> Cvalue.Model.t
val assign_return_to_lv_one_loc : with_alarms:CilE.warn_mode ->
Locals_scoping.clobbered_set ->
Cil_types.typ ->
Cil_types.lval * Locations.location * Cil_types.typ ->
Cvalue.Model.offsetmap -> Cvalue.Model.t -> Cvalue.Model.t * bool
val assign_return_to_lv : with_alarms:CilE.warn_mode ->
Locals_scoping.clobbered_set ->
Cil_types.typ ->
Cil_types.lval * Precise_locs.precise_location * Cil_types.typ ->
Cvalue.Model.offsetmap -> Cvalue.Model.t -> Cvalue.Model.t
val interp_call : with_alarms:CilE.warn_mode ->
Locals_scoping.clobbered_set ->
Value_results.Terminating_calls.key ->
Cil_types.lval option ->
Cil_types.exp ->
Cil_types.exp list ->
Cvalue.Model.t -> Cvalue.Model.t list * Value_types.cacheable
exception AlwaysOverlap
val check_non_overlapping : Cvalue.Model.t -> Cil_types.lval list -> Cil_types.lval list -> unit
val check_unspecified_sequence : Cvalue.Model.t ->
(Cil_types.stmt * Cil_types.lval list * Cil_types.lval list *
Cil_types.lval list * 'a)
list -> unit
val externalize : with_alarms:CilE.warn_mode ->
Kernel_function.t ->
return_lv:Cil_types.lval option ->
Locals_scoping.clobbered_set ->
Cvalue.Model.t -> Cvalue.V_Offsetmap.t option * Cvalue.Model.t