D (goblint.Goblint_lib.C2poDomain.D)

include sig ... end

type t = [

| `Bot
| `Lifted of C2PODomain.t

]

val equal : t -> t -> Ppx_deriving_runtime.bool

val compare : t -> t -> Ppx_deriving_runtime.int

val hash : t -> int

val tag : 'a -> 'b

val arbitrary : unit -> 'a

val lift : 'a -> [> `Lifted of 'a ]

val show : [< `Bot | `Lifted of C2PODomain.t ] -> string

val pretty : unit -> t -> Printable.Pretty.doc

val name : unit -> string

val to_yojson : [< `Bot | `Lifted of C2PODomain.t ] -> Yojson.Safe.t

val relift : 
  [< `Bot | `Lifted of C2PODomain.t ] ->
  [> `Bot | `Lifted of C2PODomain.t ]

val bot : unit -> [> `Bot ]

val is_bot : [> `Bot ] -> bool

val top : unit -> [> `Lifted of C2PODomain.t ]

val is_top : [< `Bot | `Lifted of C2PODomain.t ] -> bool

val leq : 
  [< `Bot | `Lifted of C2PODomain.t ] ->
  [< `Bot | `Lifted of C2PODomain.t ] ->
  bool

val pretty_diff : unit -> (t * t) -> Lattice.Pretty.doc

val join : [< `Bot | `Lifted of C2PODomain.t Lifted ] as 'a -> 'a -> 'a

val widen : 
  [> `Lifted of C2PODomain.t ] ->
  [> `Lifted of C2PODomain.t ] as 'a ->
  'a

val show_all : [< `Bot | `Lifted of CongruenceClosure.t ] -> string

val meet : 
  [< `Bot | `Lifted of C2PODomain.t ] ->
  [< `Bot | `Lifted of C2PODomain.t ] ->
  [> `Bot | `Lifted of C2PODomain.t ]

val narrow : 
  [> `Bot | `Lifted of C2PODomain.t ] as 'a ->
  [> `Bot | `Lifted of C2PODomain.t ] ->
  'b

val printXml : 
  'a BatInnerIO.output ->
  [< `Bot | `Lifted of C2PODomain.t ] ->
  unit

val remove_terms_containing_aux_variable : 
  CongruenceClosure.data ->
  CongruenceClosure.data

Remove terms from the data structure. It removes all terms that contain an AssignAux variable, while maintaining all equalities about variables that are not being removed.

val remove_terms_containing_return_variable : 
  CongruenceClosure.data ->
  CongruenceClosure.data

Remove terms from the data structure. It removes all terms that contain an ReturnAux variable, while maintaining all equalities about variables that are not being removed.

val remove_terms_containing_variables : 
  DuplicateVars.Var.t list ->
  CongruenceClosure.data ->
  CongruenceClosure.data

Remove terms from the data structure. It removes all terms which contain one of the "vars", while maintaining all equalities about variables that are not being removed.

val remove_terms_not_containing_variables : 
  DuplicateVars.Var.t list ->
  CongruenceClosure.data ->
  CongruenceClosure.data

Remove terms from the data structure. It removes all terms which do not contain one of the "vars", except the global vars are also kept (when vglob = true), while maintaining all equalities about variables that are not being removed.

val remove_may_equal_terms : 
  Queries.ask ->
  Z.t ->
  UnionFind.T.t ->
  CongruenceClosure.data ->
  CongruenceClosure.data

Remove terms from the data structure. It removes all terms that may be changed after an assignment to "term".

val remove_tainted_terms : 
  Queries.ask ->
  ValueDomain.AD.t ->
  CongruenceClosure.data ->
  CongruenceClosure.data

Remove terms from the data structure. It removes all terms that may point to one of the tainted addresses.

val remove_vars_not_in_scope : 
  CilType.Fundec.t ->
  CongruenceClosure.data ->
  CongruenceClosure.data

Remove terms from the data structure. It removes all terms that are not in the scope, and also those that are tmp variables.