Module type Abstract_domain.Queries

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:

When evaluating an expression, the evaluation engine asks the domains for abstract values and alarms at each lvalue (via extract_lval) and each sub-expressions (via extract_expr). In these queries:

val extract_expr : oracle:(Cil_types.exp -> value Eval.evaluated) ->
Abstract_domain.evaluation_context ->
state ->
Cil_types.exp ->
(value * origin option)
Eval.evaluated

Query function for compound expressions: extract_expr ~oracle context t exp returns the known value of exp by the state t. See above for more details on queries.

val extract_lval : oracle:(Cil_types.exp -> value Eval.evaluated) ->
Abstract_domain.evaluation_context ->
state ->
Cil_types.lval ->
Cil_types.typ ->
location ->
(value * origin option)
Eval.evaluated

Query function for lvalues: extract_lval ~oracle context t lval typ loc returns the known value stored at the location loc of the left value lval of type typ. See above for more details on queries.

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.