Module Simpler_domains

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 : Cil_types.varinfo;
   concrete : Cil_types.exp;
}
Both the formal argument of a called function and the concrete argument at a call site.
type simple_call = {
   kf : Cil_types.kernel_function;
   arguments : simple_argument list;
   rest : Cil_types.exp list;
   return : Cil_types.varinfo option;
   recursive : bool;
}
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 : Cil_types.exp -> Cvalue.V.t Eval.flagged_value Eval.or_top;
   find_loc : Cil_types.lval -> Precise_locs.precise_location Eval.or_top;
}
A simpler functional interface for valuations.
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.