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:

alarms are the set of alarms ensuring the soundness of the evaluation;
res is either `Bottom if the evaluation is impossible, or `Value (valuation, value), where value is the numeric value computed for exp, and valuation contains all the intermediate results of the evaluation. About optional arguments:
valuation is a cache of already computed expressions; empty by default.
if indeterminate is true, then the lvalues uninitialized or escaping are considered as unreduced (their reductness is not set to Reduced); false by default.

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