module Domain_mode: sig
.. end
This module defines the mode to restrict an abstract domain on specific
functions.
type
permission = {
|
read : bool ; |
|
write : bool ; |
}
Permission for an abstract domain to read/write its state.
If write
is true, the domain infers new properties when interpreting
assignments, assumptions, and logical assertions. Otherwise, it only
propagates already known properties as long as they hold.
If read
is true, the domain uses its inferred properties to improve
the evaluation of expressions by extracting information from its state.
It can also evaluate logical assertions.
type
mode = {
}
Mode for the analysis of a function
f
:
current
is the read/write permission for f
.
calls
is the read/write permission for all functions called from f
.
module Mode: sig
.. end
Datatype for modes.
type
function_mode = Kernel_function.t * mode
A function associated with an analysis mode.
module Function_Mode: Parameter_sig.Multiple_value_datatype
with type key = string
and type t = function_mode
include Datatype.S
Analysis mode for a domain.