Module type Abstract_domain.S

module type S = sig .. end

Signature for the abstract domains of the analysis.

type state

include Datatype.S_with_collections

include Abstract_domain.Lattice

Lattice Structure

include Abstract_domain.Queries

Queries

Transfer Functions

include Abstract_domain.Transfer

Transfer functions from the result of evaluations. See for more details about valuation.

Logic

Logical evaluation. This API is subject to changes.

val logic_assign : (location Eval.logic_assign * state) option ->
       location -> state -> state

logic_assign None loc state removes from state all inferred properties that depend on the memory location loc. If the first argument is not None, it contains the logical clause being interpreted and the pre-state in which the terms of the clause are evaluated. The clause can be an assigns, allocates or frees clause. loc is then the memory location concerned by the clause.

val evaluate_predicate : state Abstract_domain.logic_environment ->
       state -> Cil_types.predicate -> Alarmset.status

Evaluates a predicate to a logical status in the current state. The logic_environment contains the states at some labels and the potential variable for \result. Defined by Domain_builder.Complete: all predicates are Unknown.

val reduce_by_predicate : state Abstract_domain.logic_environment ->
       state ->
       Cil_types.predicate -> bool -> state Eval.or_bottom

reduce_by_predicate env state pred b reduces the current state by assuming that the predicate pred evaluates to b. env contains the states at some labels and the potential variable for \result. Defined by Domain_builder.Complete with no reduction.

val interpret_acsl_extension : Cil_types.acsl_extension ->
       state Abstract_domain.logic_environment ->
       state -> state

Interprets an ACSL extension. Defined by Domain_builder.Complete as the identity.

Scoping and initialization

Scoping: abstract transformers for entering and exiting blocks. The variables should be added or removed from the abstract state here. Note that the formals of a called function enter the scope through the transfer function start_call, and leave it through a call to Abstract_domain.S.leave_scope.

val enter_scope : Abstract_domain.variable_kind -> Cil_types.varinfo list -> t -> t

Introduces a list of variables in the state. At this point, the variables are uninitialized. Globals and formals of the 'main' will be initialized by Abstract_domain.S.initialize_variable and Abstract_domain.S.initialize_variable_using_type. Local variables remain uninitialized until an assignment through assign. The formal parameters of a call enter the scope through start_call.

val leave_scope : Cil_types.kernel_function -> Cil_types.varinfo list -> t -> t

Removes a list of local and formal variables from the state. The first argument is the englobing function.

val empty : unit -> t

The initial state with which the analysis start.

val initialize_variable : Cil_types.lval ->
       location -> initialized:bool -> Abstract_domain.init_value -> t -> t

initialize_variable lval loc ~initialized init_value state initializes the value of the location loc of lvalue lval in state with: – bits 0 if init_value = Zero; – any bits if init_value = Top. The boolean initialized is true if the location is initialized, and false if the location may be not initialized.

val initialize_variable_using_type : Abstract_domain.variable_kind -> Cil_types.varinfo -> t -> t

Initializes a variable according to its type. The variable can be:

a global variable on lib-entry mode.
a formal parameter of the 'main' function.
the return variable of a function specification.

Miscellaneous

Transfer functions called when entering/leaving a loop, and at each loop iteration. Defined as identity by Domain_builder.Complete.

val enter_loop : Cil_types.stmt -> state -> state

val incr_loop_counter : Cil_types.stmt -> state -> state

val leave_loop : Cil_types.stmt -> state -> state

include Abstract_domain.Reuse

val log_category : Self.category

Category for the messages about the domain. Must be created through Self.register_category.

val post_analysis : t Eval.or_bottom -> unit

This function is called after the analysis. The argument is the state computed at the return statement of the main function. The function can also access all states stored in the Store module during the analysis. If the analysis aborted, this function is not called. Defined by Domain_builder.Complete as doing nothing.

module Store: Domain_store.S  with type t := t

Storage of the states computed by the analysis.