module Make: functor (
Value
:
Value
) ->
functor (
Loc
:
Abstract_location.S
with type value = Value.t
) ->
functor (
Domain
:
Queries
with type value = Value.t
and type location = Loc.location
) ->
S
with type state = Domain.state
and type value = Value.t
and type origin = Domain.origin
and type loc = Loc.location
Generic functor.
Parameters: |
Value |
: |
Value
|
Loc |
: |
Abstract_location.S with type value = Value.t
|
Domain |
: |
Queries with type value = Value.t
and type location = Loc.location
|
|
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 can_copy : ?valuation:Valuation.t ->
is_ret:bool ->
state ->
Kernel_function.t ->
Cil_types.lval ->
Cil_types.exp ->
(Cil_types.lval option * Valuation.t) Eval.evaluated
can_copy is_ret state kf lv e
checks whether assigning
e
to
lv
inside function
kf
and in the context of
state
can be a simple copy of an lval or must be an assignment
(see
Eval.assigned
for more information).
is_ret
indicates whether the assigned expr is in fact the value
returned by a callee.
Returns Some rlv
if the assignment can be seen as a copy from rlv to lv,
and
None
otherwise
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_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