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 ->
?reduction:bool ->
state ->
Cil_types.exp ->
(Valuation.t * value) Eval.evaluated
evaluate ~valuation state expr
evaluates the expression expr
in the
state state
, and returns the pair result, alarms
, where:
alarms
are the set of alarms ensuring the soundness of the evaluation;result
is either `Bottom if the evaluation leads to an error,
or `Value (valuation, value), where value
is the numeric value computed
for the expression expr
, and valuation
contains all the intermediate
results of the evaluation.
The valuation
argument is a cache of already computed expressions.
It is empty by default.
The reduction
argument allows deactivating the backward reduction
performed after the forward evaluation.val copy_lvalue : ?valuation:Valuation.t ->
state ->
Cil_types.lval ->
(Valuation.t * value Eval.flagged_value)
Eval.evaluated
Computes the value of a lvalue, with possible indeterminateness: the
returned value may be uninitialized, or contain escaping addresses.
Also returns the alarms resulting of the evaluation of the lvalue location,
and a valuation containing all the intermediate results of the evaluation.
The valuation
argument is a cache of already computed expressions.
It is empty 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
reduce ~valuation state expr positive
evaluates the expression expr
in the state state
, and then reduces the valuation
such that
the expression expr
evaluates to a zero or a non-zero value, according
to positive
. By default, the empty valuation is used.
val assume : ?valuation:Valuation.t ->
state ->
Cil_types.exp ->
value -> Valuation.t Eval.or_bottom
assume ~valuation state expr value
assumes in the valuation
that
the expression expr
has the value value
in the state state
,
and backward propagates this information to the subterm of expr
.
If expr
has not been already evaluated in the valuation
, its forward
evaluation takes place first, but the alarms are dismissed. By default,
the empty valuation is used.
The function returns the updated valuation, or bottom if it discovers
a contradiction.
val split_by_evaluation : Cil_types.exp ->
Integer.t list ->
state list ->
(Integer.t * state list * bool) list * state list
val check_non_overlapping : state ->
Cil_types.lval list -> Cil_types.lval list -> unit Eval.evaluated
val eval_function_exp : Cil_types.exp ->
?args:Cil_types.exp list ->
state ->
(Kernel_function.t * Valuation.t) list Eval.evaluated
Evaluation of the function argument of a Call
constructor