Frama-C:
Plug-ins:
Libraries:

Frama-C API - Queries

include Abstract_domain.Queries
type state

Domain state.

type context

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.

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, 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.

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.

Query 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_bottom

backward_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.

val reduce_further : state -> Eval.exp -> value -> (Eval.exp * value) list

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_bottom

Returns the current context to be used by value abstractions for the evaluation of expressions or lvalues. Defined by Domain_builder.Complete with no context.

include Frama_c_kernel.Datatype.S with type t = state
include Frama_c_kernel.Datatype.S_no_copy with type t = state
include Frama_c_kernel.Datatype.Ty with type t = state
type t = state
val datatype_name : string

Unique name of the datatype.

val datatype_descr : t Frama_c_kernel.Descr.t

Datatype descriptor.

Packed version of the descriptor.

val reprs : t list

List of representants of the descriptor.

val equal : t -> t -> bool

Equality: same spec than Stdlib.(=).

val compare : t -> t -> int

Comparison: same spec than Stdlib.compare.

val hash : t -> int

Hash function: same spec than Hashtbl.hash.

val pretty : Stdlib.Format.formatter -> t -> unit

Pretty print each value in an user-friendly way.

val mem_project : (Frama_c_kernel.Project_skeleton.t -> bool) -> t -> bool

mem_project f x must return true iff there is a value p of type Project.t in x such that f p returns true.

val copy : t -> t

Deep copy: no possible sharing between x and copy x.