Module Function_Froms

module Function_Froms: sig .. end

Datastructures and common operations for the results of the From plugin.

A From table is internally represented as a Lmap of DepsOrUnassigned. However, the API mostly hides this fact, and exports access functions that take or return Deps.t values. This way, the user needs not understand the subtleties of DepsBottom/Unassigned/MaybeAssigned.

module Deps: sig .. end

module DepsOrUnassigned: sig .. end

module Memory: sig .. end

type froms = {

	`deps_return : Memory.return;`	`(*`	Dependencies for the returned value	`*)`
	`deps_table : Memory.t;`	`(*`	Dependencies on all the zones modified by the function	`*)`

}

include Datatype.S

val join : froms -> froms -> froms

val top : froms

Display dependencies of a function, using the function's type to improve readability

val pretty_with_type : Cil_types.typ -> froms Pretty_utils.formatter

Display dependencies of a function, using the function's type to improve readability, separating direct and indirect dependencies

val pretty_with_type_indirect : Cil_types.typ -> froms Pretty_utils.formatter

val outputs : froms -> Locations.Zone.t

Extract the left part of a from result, ie. the zones that are written

val inputs : ?include_self:bool -> froms -> Locations.Zone.t

Extract the right part of a from result, ie. the zones on which the written zones depend. If include_self is true, and the from is of the form x FROM y (and SELF), x is added to the result; default value is false.