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