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.