Module ConfigGating.ConfigGuards

For each config, the set of values it may have if this point is reached. Absent config = unconstrained (may be any value). Join = union of possible value sets per config; if a config becomes unconstrained (both True and False are possible), it is removed. Empty map = no config is constrained = code always executes.

module M : sig ... end
type t = BranchVal.t M.t
val pp : F.formatter -> BranchVal.t M.t -> unit
val empty : 'a M.t
val is_empty : 'a M.t -> bool
val add : M.key -> 'a -> 'a M.t -> 'a M.t
val leq : lhs:BranchVal.t M.t -> rhs:BranchVal.t M.t -> bool
val widen : prev:BranchVal.t M.t -> next:BranchVal.t M.t -> num_iters:'a -> BranchVal.t M.t