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 : Eval.logic_assign ->
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.
include Abstract_domain.Recycle
val log_category : Value_parameters.category
Category for the messages about the domain.
Must be created through Value_parameters.register_category
.