package goblint

  1. Overview
  2. Docs
Static analysis framework for C

Install 

dune-project
 Dependency

goblint.in.tum.de Readme Changelog Edit opam file Versions (9)

Authors

  1. S
    Simmo Saan
  2. M
    Michael Schwarz
  3. J
    Julian Erhard
  4. S
    Sarah Tilscher
  5. K
    Karoliine Holter
  6. R
    Ralf Vogler
  7. K
    Kalmer Apinis
  8. V
    Vesal Vojdani

Maintainers

  1. S
    Simmo Saan <simmo.saan@gmail.com>
  2. M
    Michael Schwarz <michael.schwarz93@gmail.com>
  3. K
    Karoliine Holter <karoliine.holter@ut.ee>

Sources

goblint-2.6.0.tbz
sha256=20d5b7332a9f6072ab9ba86c4a53b898eaf681286c56a8805c41850bbf3ddf41
sha512=7c7685cfcd9aa866bc40e813df2bfcb3c79b3d40e615d8d6d0939c5798b9d70dd7f2ba87a741f5ba0ce891e9d254627207fb28057f1f2f6611e4e0d128fd6a71

doc/goblint.lib/Goblint_lib/UnionFind/T/index.html

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.

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".

Use query EvalInt for an expression.

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

From a offset, compute the index in bits

Convert a Cil offset to an integer offset.

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_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