module type Queries =sig
..end
Extraction of information: queries for values or locations inferred by a domain about expressions and lvalues. Used in the evaluation of expressions and lvalues.
type
state
Domain state.
type
value
Numerical values to which the expressions are evaluated.
type
location
Abstract memory locations associated to left values.
type
origin
The origin
is used by the domain combiners to track the origin
of a value. An abstract domain can always use a dummy type unit for
origin, or use it to encode some specific information about a value.
Queries functions return a pair of:
exp
. Alarmset.all
is always a sound over-approximation of these
alarms.v
is an over-approximation of the abstract
value of the expression exp
, and o
is the origin of the value.val extract_expr : (Cil_types.exp -> value Eval.evaluated) ->
state ->
Cil_types.exp ->
(value * origin)
Eval.evaluated
Query function for compound expressions:
eval oracle t exp
returns the known value of exp
by the state t
.
oracle
is an evaluation function and can be used to find the answer
by evaluating some others expressions, especially by relational domain.
No recursive evaluation should be done by this function.
val extract_lval : (Cil_types.exp -> value Eval.evaluated) ->
state ->
Cil_types.lval ->
Cil_types.typ ->
location ->
(value * origin)
Eval.evaluated
Query function for lvalues:
find oracle t lval typ loc
returns the known value stored at
the location loc
of the left value lval
of type typ
.
val backward_location : state ->
Cil_types.lval ->
Cil_types.typ ->
location ->
value ->
(location * value)
Eval.or_bottom
backward_location state lval typ loc v
reduces the location loc
of the
lvalue lval
of type typ
, so that only the locations that may have value
v
are kept.
The returned location must be included in loc
, but it is always sound
to return loc
itself.
Also returns the value that may have the returned location, if not bottom.
val reduce_further : state ->
Cil_types.exp ->
value ->
(Cil_types.exp * value) list
Given a reduction expr
= value
, provides more reductions that may
be performed.