Module type Abstract_domain.Queries

module type Queries = sig .. end

Queries for values stored by a domain about expressions or locations. 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:

the set of alarms that ensures the of the soundness of the evaluation of exp. Alarmset.all is always a sound over-approximation of these alarms.
a value for the expression, which can be:
`Bottom if its evaluation is infeasible;
`Value (v, o) where 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.