Module Goblint_lib.Access

Memory accesses and their manipulation.

module M = Messages
val is_ignorable_comp_name : string -> bool
val is_ignorable_attrs : GoblintCil.attribute list -> bool
val is_ignorable_type : GoblintCil.typ -> bool
val is_ignorable_type_offset : GoblintCil.typ -> 'a Offset.t -> bool
val is_ignorable_typsig : GoblintCil.typsig -> bool

is_ignorable_type for typsig.

val is_ignorable_typsig_offset : GoblintCil.typsig -> 'a Offset.t -> bool

is_ignorable_type_offset for typsig.

val is_ignorable_mval : (GoblintCil.varinfo * 'a Offset.t) -> bool
val is_ignorable_memo : ([< `Type of GoblintCil.typsig | `Var of GoblintCil.varinfo ] * 'a Offset.t) -> bool
module TSH : sig ... end
val typeVar : GoblintCil.varinfo TSH.t
val typeIncl : GoblintCil.fieldinfo TSH.t
val collect_direct_arithmetic : bool Batteries.ref
val init : GoblintCil.file -> unit
val reset : unit -> unit
type acc_typ = [
  1. | `Type of CilType.Typ.t
  2. | `Struct of CilType.Compinfo.t * Offset.Unit.t
]

Old access type inferred from an expression.

val equal_acc_typ : acc_typ -> acc_typ -> Ppx_deriving_runtime.bool
val compare_acc_typ : acc_typ -> acc_typ -> Ppx_deriving_runtime.int
val hash_acc_typ : acc_typ -> int
module MemoRoot : sig ... end
module Memo : sig ... end

Memory location of an access.

val get_type : GoblintCil.typ Stdlib.Lazy.t -> GoblintCil.exp -> acc_typ
val get_val_type : GoblintCil.exp -> acc_typ
val add_one : side: (([< `Type of GoblintCil.typsig | `Var of CilType.Varinfo.t ] as 'a * Offset.Unit.t) -> unit) -> ('a * Offset.Unit.t) -> unit

Add access to Memo after distributing.

val add_distribute_outer : side: (([ `Type of GoblintCil.typsig | `Var of CilType.Varinfo.t ] * Offset.Unit.t) -> unit) -> side_empty: (([ `Type of GoblintCil.typsig | `Var of CilType.Varinfo.t ] * Offset.Unit.t) -> unit) -> GoblintCil.typsig -> Offset.Unit.t -> unit

Distribute empty access set for type-based access to variables and containing fields. Empty access sets are needed for prefix-type_suffix race checking.

val add : side: (([ `Type of GoblintCil.typsig | `Var of CilType.Varinfo.t ] * Offset.Unit.t) -> unit) -> side_empty: (([ `Type of GoblintCil.typsig | `Var of CilType.Varinfo.t ] * Offset.Unit.t) -> unit) -> CilType.Exp.t -> (CilType.Varinfo.t * CilType.Offset.t) option -> unit

Add access to known variable with offsets or unknown variable from expression.

Distribute to AddrOf of all read lvals in subexpressions.

val distribute_access_lval : (GoblintCil.exp -> unit) -> GoblintCil.lval -> unit
val distribute_access_lval_addr : (GoblintCil.exp -> unit) -> GoblintCil.lval -> unit
val distribute_access_offset : (GoblintCil.exp -> unit) -> GoblintCil.offset -> unit
val distribute_access_exp : (GoblintCil.exp -> unit) -> GoblintCil.exp -> unit
val distribute_access_type : (GoblintCil.exp -> unit) -> GoblintCil.typ -> unit
module A : sig ... end
module AS : sig ... end
val may_race : A.t -> A.t -> bool

Check if two accesses may race.

module WarnAccs : sig ... end

Access sets for race detection and warnings.

val group_may_race : WarnAccs.t -> AS.t list
val race_conf : AS.t -> Batteries.Int.t option
val is_all_safe : bool Batteries.ref
val incr_summary : safe:int Batteries.ref -> vulnerable:int Batteries.ref -> unsafe:int Batteries.ref -> AS.t list -> unit
val print_accesses : ([< `Type of GoblintCil.typsig & 'a | `Var of CilType.Varinfo.t ] * Offset.Unit.t) -> AS.t list -> unit
val warn_global : safe:int Batteries.ref -> vulnerable:int Batteries.ref -> unsafe:int Batteries.ref -> WarnAccs.t -> ([< `Type of GoblintCil.typsig & 'a | `Var of CilType.Varinfo.t ] * Offset.Unit.t) -> unit