Module type Evaluation.S

module type S = sig .. end

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