Module UnionFind.T

The terms consist of address constants and dereferencing function with sum of an integer. The dereferencing function is parametrized by the size of the element in the memory. We store the CIL expression of the term in the data type, such that it it easier to find the types of the dereferenced elements. Also so that we can easily convert back from term to Cil expression.

type exp = GoblintCil.Cil.exp
val bitsSizeOfPtr : unit -> Z.t
type t = term
val equal : t -> t -> Ppx_deriving_runtime.bool
val hash : t -> int
val compare : t -> t -> Ppx_deriving_runtime.int
type v_prop = prop
val equal_v_prop : v_prop -> v_prop -> Ppx_deriving_runtime.bool
val hash_v_prop : v_prop -> int
val compare_v_prop : v_prop -> v_prop -> Ppx_deriving_runtime.int
val props_equal : v_prop list -> v_prop list -> bool
val is_addr : term -> bool
exception UnsupportedCilExpression of string
val get_size_in_bits : GoblintCil.Cil.typ -> Z.t
val show_type : GoblintCil.exp -> string
val show : t -> string
val show_prop : prop -> string
val is_subterm : t -> t -> bool

Returns true if the first parameter is a subterm of the second one.

val get_var : term -> DuplicateVars.Var.t
val contains_variable : DuplicateVars.Var.t list -> term -> bool

Returns true if the second parameter contains one of the variables defined in the list "variables".

val eval_int : Queries.ask -> GoblintCil.exp -> IntDomain.IntDomTuple.int_t

Use query EvalInt for an expression.

val eval_int_opt : Queries.ask -> GoblintCil.exp -> IntDomain.IntDomTuple.int_t option
val type_of_element : GoblintCil.Cil.typ -> GoblintCil.typ option

Returns Some type for a pointer to a type and None if the result is not a pointer.

val get_element_size_in_bits : GoblintCil.Cil.typ -> Z.t

Returns the size of the type. If typ is a pointer, it returns the size of the elements it points to. If typ is an array, it returns the size of the elements of the array (even if it is a multidimensional array. Therefore get_element_size_in_bits int[][][] = sizeof(int)).

val is_struct_type : GoblintCil.Cil.typ -> bool
val is_struct_ptr_type : GoblintCil.Cil.typ -> bool
val aux_term_of_varinfo : Goblint_lib__DuplicateVars.VarType.t -> term
val term_of_varinfo : Goblint_lib__DuplicateVars.VarType.t -> term
val offset_to_index : ?typ:GoblintCil.typ -> PreValueDomain.Offs.t -> IntDomain.IntDomTuple.t

From a offset, compute the index in bits

val cil_offs_to_idx : Queries.ask -> GoblintCil.offset -> GoblintCil.Cil.typ -> IntDomain.IntDomTuple.t

Convert a Cil offset to an integer offset.

val z_of_offset : Queries.ask -> GoblintCil.offset -> GoblintCil.Cil.typ -> IntDomain.IntDomTuple.int_t

Convert an offset to an integer of Z, if posible. Otherwise, this throws UnsupportedCilExpression.

val can_be_dereferenced : GoblintCil.Cil.typ -> bool
val type_of_term : term -> GoblintCil.typ
val to_cil : term -> GoblintCil.exp
val default_int_type : GoblintCil.ikind
val to_cil_constant : Z.t -> GoblintCil.Cil.typ option -> GoblintCil.exp

Returns a Cil expression which is the constant z divided by the size of the elements of t.

val to_cil_sum : Z.t -> GoblintCil.exp -> GoblintCil.exp

Returns the integer offset of a field of a struct.

val is_field : GoblintCil.offset -> bool
val add_index_to_exp : GoblintCil.exp -> GoblintCil.offset -> GoblintCil.exp
val check_valid_pointer : GoblintCil.exp -> bool

Returns true if the Cil expression represents a 64 bit data type which is not a float. So it must be either a pointer or an integer that has the same size as a pointer.

val filter_valid_pointers : prop list -> prop list

Only keeps the variables that are actually pointers (or 64-bit integers).

val dereference_exp : GoblintCil.exp -> Z.t -> GoblintCil.exp

Get a Cil expression that is equivalent to *(exp + offset), by taking into account type correctness.

val get_size : term -> Z.t
val of_offset : Queries.ask -> term -> GoblintCil.offset -> GoblintCil.Cil.typ -> GoblintCil.exp -> term
val of_lval : Queries.ask -> GoblintCil.lval -> term
val of_cil_neg : Queries.ask -> bool -> GoblintCil.exp -> term option * GoblintCil__.Cilint.cilint option

Converts the negation of the expression to a term if neg = true. If neg = false then it simply converts the expression to a term.

val of_cil : Queries.ask -> GoblintCil.exp -> term option * GoblintCil__.Cilint.cilint option

Convert the expression to a term, and additionally check that the term is 64 bits. If it's not a 64bit pointer, it returns None, None.

val map_z_opt : ('a -> 'b -> 'c) -> 'a -> ('d * 'b option) -> 'd * 'c option
val two_terms_of_cil : Queries.ask -> bool -> GoblintCil.exp -> (term option * GoblintCil__.Cilint.cilint option) * (term option * GoblintCil__.Cilint.cilint option)

Converts a cil expression e = "t1 + off1 - (t2 + off2)" to two terms (Some t1, Some off1), (Some t2, Some off2)

val prop_of_cil : Queries.ask -> GoblintCil.Cil.exp -> bool -> prop list

`prop_of_cil e pos` parses the expression `e` (or `not e` if `pos = false`) and returns a list of length 1 with the parsed expresion or an empty list if the expression can't be expressed with the type `prop`.

val prop_to_cil : prop -> GoblintCil.exp