Module Eval_stmt

module Eval_stmt: sig .. end
Value analysis of statements and functions bodies

val compute_call_ref : (Kernel_function.t ->
recursive:bool ->
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
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 ->
Cil_types.typ ->
Cil_types.exp -> Locations.Location.t -> Cvalue.Model.t * bool
val lval_to_precise_loc_state_for_writing : with_alarms:CilE.warn_mode ->
Cvalue.Model.t ->
Cil_types.lval ->
Cvalue.Model.t * Precise_locs.precise_location * Cil_types.typ
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.V_Offsetmap.t -> Cvalue.Model.t -> Cvalue.Model.t
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.V_Offsetmap.t -> Cvalue.Model.t -> Cvalue.Model.t
val reduce_actuals_by_formals : Cil_types.varinfo list ->
Cil_types.exp list -> Cvalue.Model.t -> Cvalue.Model.t
This function unbinds formals in state. Also, when possible, given a formal f, it reduces the corresponding actual act_f to the value of f in state. It it is used after a call to clean up the state, and to gain some informations on the actuals.
val interp_call : with_alarms:CilE.warn_mode ->
Locals_scoping.clobbered_set ->
Cil_types.stmt ->
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