module type S =sig
..end
Signature for the abstract domains of the analysis.
type
state
include Datatype.S_with_collections
include Abstract_domain.Lattice
include Abstract_domain.Queries
include Abstract_domain.Transfer
Transfer functions from the result of evaluations. See for more details about valuation.
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.
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.
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:
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 : Value_parameters.category
Category for the messages about the domain.
Must be created through Value_parameters.register_category
.