Module Absint.TransferFunctions

Transfer functions that push abstract states across instructions. A typical client should implement the Make signature to allow the transfer functions to be used with any kind of CFG.

module type S = sig ... end
module type SIL = sig ... end
module type HIL = sig ... end
type join_policy_t =
  1. | UnderApproximateAfter of int

When the set of disjuncts gets bigger than n then just stop adding new states to it, drop any further states on the floor. This corresponds to an under-approximation/bounded approach.

type widen_policy_t =
  1. | UnderApproximateAfterNumIterations of int
module type DisjunctiveConfig = sig ... end
module type DisjReady = sig ... end