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

module Transfer: functor (Valuation : Abstract_domain.Valuation  with type value = value
                             and type origin = origin
                             and type loc = location) -> Abstract_domain.Transfer  with type state := t
                and type value := value
                and type location := location
                and type valuation := Valuation.t

Transfer functions from the result of evaluations.

Logic

Logical evaluation. This API is subject to changes.

val logic_assign : Cil_types.from ->
       location ->
       pre:state ->
       state -> state

logic_assign from loc_asgn pre state applies the effect of the assigns ... \from ... clause from to state. pre is the state before the assign clauses, in which the terms of the clause are evaluated. loc_asgn is the result of the evaluation of the assigns part of from in pre.

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.

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.

Miscellaneous

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

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

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

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

Initialization

val empty : unit -> t

The initial state with which the analysis start.

val introduce_globals : Cil_types.varinfo list -> t -> t

Introduces the list of global variables in the state. At this point, these variables are uninitialized: they will be initialized through the two functions below.

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.init_kind -> Cil_types.varinfo -> t -> t

Initializes a variable according to its type. TODO: move some parts of the cvalue implementation of this function in the generic engine.

val filter_by_bases : Base.Hptset.t -> t -> t

Mem exec.

val reuse : current_input:t -> previous_output:t -> t