AbstractInterpreter (infer.Absint.AbstractInterpreter)

module F = Stdlib.Format

module VisitCount : sig ... end

module State : sig ... end

module type S = sig ... end

type of an intraprocedural abstract interpreter

module type Make =
  functor (TransferFunctions : 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 DisjunctiveMetadata : sig ... end

used internally to compute various metrics related to MakeDisjunctive analyses; this can be queried with get_cfg_metadata below at the end of the analysis of each procedure

module MakeDisjunctive
  (T : TransferFunctions.DisjReady)
  (DConfig : TransferFunctions.DisjunctiveConfig) : 
  sig ... end

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.

module type TransferFunctions = sig ... end

module type MakeExceptional =
  functor (T : TransferFunctions) ->
  S with module TransferFunctions = T

module MakeBackwardRPO : MakeExceptional

module MakeBackwardWTO : MakeExceptional