Module Goblint_lib.BaseDomain

Full domain of Base analysis.

module CPA : sig ... end
module PartDeps : sig ... end
module WeakUpdates : sig ... end

Maintains a set of local variables that need to be weakly updated, because multiple reachable copies of them may

type 'a basecomponents_t = {
  1. cpa : CPA.t;
  2. deps : PartDeps.t;
  3. weak : WeakUpdates.t;
  4. priv : 'a;
}
val equal_basecomponents_t : 'a. ('a -> 'a -> Ppx_deriving_runtime.bool) -> 'a basecomponents_t -> 'a basecomponents_t -> Ppx_deriving_runtime.bool
val compare_basecomponents_t : 'a. ('a -> 'a -> Ppx_deriving_runtime.int) -> 'a basecomponents_t -> 'a basecomponents_t -> Ppx_deriving_runtime.int
val hash_basecomponents_t : ('a -> int) -> 'a basecomponents_t -> int
val relift_basecomponents_t : ('a -> 'a) -> 'a basecomponents_t -> 'a basecomponents_t
val is_top_basecomponents_t : ('a -> bool) -> 'a basecomponents_t -> bool
val top_basecomponents_t : (unit -> 'a) -> unit -> 'a basecomponents_t
val is_bot_basecomponents_t : ('a -> bool) -> 'a basecomponents_t -> bool
val bot_basecomponents_t : (unit -> 'a) -> unit -> 'a basecomponents_t
val narrow_basecomponents_t : ('a -> 'a -> 'a) -> 'a basecomponents_t -> 'a basecomponents_t -> 'a basecomponents_t
val widen_basecomponents_t : ('a -> 'a -> 'a) -> 'a basecomponents_t -> 'a basecomponents_t -> 'a basecomponents_t
val meet_basecomponents_t : ('a -> 'a -> 'a) -> 'a basecomponents_t -> 'a basecomponents_t -> 'a basecomponents_t
val join_basecomponents_t : ('a -> 'a -> 'a) -> 'a basecomponents_t -> 'a basecomponents_t -> 'a basecomponents_t
val leq_basecomponents_t : ('a -> 'a -> bool) -> 'a basecomponents_t -> 'a basecomponents_t -> bool
module BaseComponents (PrivD : Lattice.S) : sig ... end
module type ExpEvaluator = sig ... end
module DomFunctor (PrivD : Lattice.S) (ExpEval : ExpEvaluator with type t = BaseComponents(PrivD).t) : sig ... end
module DomWithTrivialExpEval (PrivD : Lattice.S) : sig ... end