Functor Evaluation.Make

module Make: 
functor (Value : Value) ->
functor (Loc : Abstract_location.S with type value = Value.t) ->
functor (Domain : Abstract_domain.Queries with type value = Value.t and type location = Loc.location) -> S with type state = Domain.state and type value = Value.t and type origin = Domain.origin and type loc = Loc.location
Generic functor.
Parameters:
Value : Value
Loc : Abstract_location.S with type value = Value.t
Domain : Abstract_domain.Queries with type value = Value.t and type location = Loc.location

type state 
State of abstract domain.
type value 
Numeric values to which the expressions are evaluated.
type origin 
Origin of values.
type loc 
Location of an lvalue.
module Valuation: Valuation  with type value = value
                                and type origin = origin
                                and type loc = loc
Results of an evaluation: the results of all intermediate calculation (the value of each expression and the location of each lvalue) are cached here.
val evaluate : ?valuation:Valuation.t ->
?indeterminate:bool ->
?reduction:bool ->
state ->
Cil_types.exp ->
(Valuation.t * value) Eval.evaluated
evaluate ~valuation ~indeterminate state exp evaluates the expression exp in the state state, and returns the pair res, alarms, where:
val lvaluate : ?valuation:Valuation.t ->
for_writing:bool ->
state ->
Cil_types.lval ->
(Valuation.t * loc * Cil_types.typ) Eval.evaluated
lvaluate ~valuation ~for_writing state lval evaluates the left value lval in the state state. Same general behavior as evaluate above but evaluates the lvalue into a location and its type. The boolean for_writing indicates whether the lvalue is evaluated to be read or written. It is useful for the emission of the alarms, and for the reduction of the location.
val reduce : ?valuation:Valuation.t ->
state ->
Cil_types.exp -> bool -> Valuation.t Eval.evaluated
val loc_size : loc -> Int_Base.t
val reinterpret : Cil_types.exp ->
Cil_types.typ -> value -> value Eval.evaluated
val do_promotion : src_typ:Cil_types.typ ->
dst_typ:Cil_types.typ ->
Cil_types.exp -> value -> value Eval.evaluated
val split_by_evaluation : Cil_types.exp ->
Integer.t list ->
state list ->
(Integer.t * state list * bool) list * state list
val check_copy_lval : Cil_types.lval * loc ->
Cil_types.lval * loc -> bool Eval.evaluated
val check_non_overlapping : state ->
Cil_types.lval list -> Cil_types.lval list -> unit Eval.evaluated
val eval_function_exp : Cil_types.exp ->
state ->
(Kernel_function.t * Valuation.t) list Eval.evaluated
Evaluation of the function argument of a Call constructor