Module `Absint__AbstractInterpreter`

module VisitCount : sig ... end

module State : sig ... end

module type S = sig ... end: type of an intraprocedural abstract interpreter

module type Make = functor (TransferFunctions : Absint.TransferFunctions.SIL) -> S with module TransferFunctions = TransferFunctions

module MakeRPO : Make: create an intraprocedural abstract interpreter from transfer functions using the reverse post-order scheduler

module MakeWTO : Make: create an intraprocedural abstract interpreter from transfer functions using Bourdoncle's strongly connected component weak topological order

module MakeDisjunctive : functor (T : Absint.TransferFunctions.DisjReady) -> functor (DConfig : Absint.TransferFunctions.DisjunctiveConfig) -> S with type TransferFunctions.analysis_data = T.analysis_data and module TransferFunctions.CFG = T.CFG and type TransferFunctions.Domain.t = T.Domain.t list: In the disjunctive interpreter, the domain is a set of abstract states representing a disjunction between these states. The transfer functions are executed on each state in the disjunct independently. The join on the disjunctive state is governed by the policy described in DConfig.