Frama-C API - Simpler_domains
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.
Both the formal argument of a called function and the concrete argument at a call site.
type simple_call = {kf : Frama_c_kernel.Cil_types.kernel_function;arguments : simple_argument list;rest : Eval.exp list;return : Frama_c_kernel.Cil_types.varinfo option;
}Simple information about a function call.
module type Minimal = sig ... endSimplest interface for an abstract domain. No exchange of information with the other abstractions of Eva.
module type Minimal_with_datatype = sig ... endThe simplest interface of domains, equipped with a frama-c datatype.
type cvalue_valuation = {find : Eval.exp -> Frama_c_kernel.Cvalue.V.t Eval.flagged_value Eval.or_top;find_loc : Eval.lval -> Frama_c_kernel.Precise_locs.precise_location Eval.or_top;
}A simpler functional interface for valuations.
type precise_loc = Frama_c_kernel.Precise_locs.precise_locationtype cvalue = Frama_c_kernel.Cvalue.V.tmodule type Simple_Cvalue = sig ... endA simple interface allowing the abstract domain to use the value and location abstractions computed by the other domains. Only the Cvalue.V and the the Precise_locs abstractions are available in this interface, on the transfer functions for assignment, assumption and at the call sites. On the other hand, the abstract domain cannot assist the computation of these value and location abstractions. The communication is thus unidirectional, from other domains to these simpler domains.