MayBeEqual (goblint.Goblint_lib.CongruenceClosure.MayBeEqual)

module AD = ValueDomain.AD

val dummy_var : GoblintCil.typ -> Goblint_lib__UnionFind.term

val dummy_lval_print : GoblintCil.typ -> GoblintCil.exp

val return_var : GoblintCil.typ -> Goblint_lib__UnionFind.term

val ask_may_point_to : 
  Queries.ask ->
  GoblintCil.exp ->
  ValueDomain.AD.t Queries.result

val may_point_to_all_equal_terms : 
  Queries.ask ->
  GoblintCil.exp ->
  data ->
  TMap.key ->
  Z.t ->
  AD.t

Ask MayPointTo not only for the term `term`, but also for all terms that are in the same equivalence class as `term`. Then meet the result.

val may_point_to_address : 
  Queries.ask ->
  AD.t ->
  TMap.key ->
  Z.t ->
  data ->
  bool

Find out if an addresse is possibly equal to one of the addresses in `addresses` by using the MayPointTo query.

val may_point_to_same_address : 
  Queries.ask ->
  T.t ->
  T.t ->
  Z.t ->
  data ->
  bool

Find out if two addresses `t1` and `t2` are possibly equal by using the MayPointTo query.

val may_be_equal : Queries.ask -> data -> Z.t -> term -> term -> bool

Returns true iff by assigning to t1, the value of t2 could change. The parameter s is the size in bits of the variable t1 we are assigning to.

val may_point_to_one_of_these_addresses : 
  Queries.ask ->
  AD.t ->
  data ->
  term ->
  bool

Returns true if `t2` or any subterm of `t2` may possibly point to one of the addresses in `addresses`.