module Simpler_domains:sig
..end
Simplified interfaces for abstract domains. Complete abstract domains can be
built from these interfaces through the functors in Domain_builder
. More
documentation can be found on the complete interface of abstract domains,
in Abstract_domain
.
type
simple_argument = {
|
formal : |
|
concrete : |
}
Both the formal argument of a called function and the concrete argument at a call site.
type
simple_call = {
|
kf : |
|
arguments : |
|
rest : |
|
return : |
}
Simple information about a function call.
module type Minimal =sig
..end
Simplest interface for an abstract domain.
module type Minimal_with_datatype =sig
..end
The simplest interface of domains, equipped with a frama-c datatype.
type
cvalue_valuation = {
|
find : |
|
find_loc : |
}
A simpler functional interface for valuations.
typeprecise_loc =
Precise_locs.precise_location
typecvalue =
Cvalue.V.t
module type Simple_Cvalue =sig
..end
A simple interface allowing the abstract domain to use the value and location abstractions computed by the other domains.