Abstract_domain.QueriesExtraction of information: queries for values or locations inferred by a domain about expressions and lvalues. Used in the evaluation of expressions and lvalues.
Domains can optionally provide a context to be used by value abstractions when evaluating expressions. This can be safely ignored for most domains. Defined as unit (no context) by Domain_builder.Complete.
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, which can be None.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:
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.context record gives some information about the current evaluation.val extract_expr :
oracle:(Eval.exp -> value Eval.evaluated) ->
evaluation_context ->
state ->
Eval.exp ->
(value * origin option) Eval.evaluatedQuery 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:(Eval.exp -> value Eval.evaluated) ->
evaluation_context ->
state ->
Eval.lval ->
location ->
(value * origin option) Eval.evaluatedQuery function for lvalues: extract_lval ~oracle context t lval loc returns the known value stored at the location loc of the left value lval. See above for more details on queries.
val backward_location :
state ->
Eval.lval ->
location ->
value ->
(location * value) Eval.or_bottombackward_location state lval typ loc v reduces the location loc of the lvalue lval, 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. Defined by Domain_builder.Complete with no reduction.
Given a reduction expr = value, provides more reductions that may be performed. Defined by Domain_builder.Complete with no reduction.
val build_context : state -> context Eval.or_bottomReturns the current context to be used by value abstractions for the evaluation of expressions or lvalues. Defined by Domain_builder.Complete with no context.