module Eval: Evaluation.S
with type state = Dom.t
and type value = Val.t
and type loc = Loc.location
and type origin = Dom.origin
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 to_domain_valuation : Valuation.t ->
(value, loc, origin)
Abstract_domain.valuation
Evaluation functions store the results of an evaluation into Valuation.t
maps. Abstract domains read these results from Abstract_domain.valuation
records. This function converts the former into the latter.
val evaluate : ?valuation:Valuation.t ->
?reduction:bool ->
?subdivnb:int ->
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.
Optional arguments are:
valuation
is a cache of already computed expressions; empty by default.
reduction
allows the deactivation of the backward reduction performed
after the forward evaluation; true by default.
subdivnb
is the maximum number of subdivisions performed on non-linear
sub-expressions of expr
. If a lvalue occurs several times in expr
,
its value can be split up to subdivnb
times to gain more precision.
Set to the value of the option -eva-subdivide-non-linear by default.
val copy_lvalue : ?valuation:Valuation.t ->
?subdivnb:int ->
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.
subdivnb
is the maximum number of subdivisions performed on non-linear
expressions.
val lvaluate : ?valuation:Valuation.t ->
?subdivnb:int ->
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.
subdivnb
is the maximum number of subdivisions performed on non-linear
expressions (including the possible pointer and offset of the lvalue).
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 eval_function_exp : ?subdivnb:int ->
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
val interpret_truth : alarm:(unit -> Alarms.t) ->
'a -> 'a Abstract_value.truth -> 'a Eval.evaluated