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;`

}

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.

type precise_loc = Precise_locs.precise_location

type cvalue = 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.