Module Eval_stmt

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

val compute_call_ref : (Cil_types.kernel_function ->
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 do_assign : with_alarms:CilE.warn_mode ->
Cil_types.kernel_function ->
Locals_scoping.clobbered_set ->
Cvalue.Model.t -> Cil_types.lval -> Cil_types.exp -> Cvalue.Model.t
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 * Cil_types.stmt Pervasives.ref list)
list -> unit
val externalize : with_alarms:CilE.warn_mode ->
Cil_types.kernel_function ->
return_lv:Cil_types.lval option ->
Locals_scoping.clobbered_set ->
Cvalue.Model.t -> Cvalue.V_Offsetmap.t option * Cvalue.Model.t