Module Goblint_lib.Access

Memory accesses and their manipulation.

module M = Messages
val is_ignorable_type : GoblintCil.typ -> bool
val is_ignorable : (GoblintCil.varinfo * 'a) option -> bool
module TSH : sig ... end
val typeVar : GoblintCil.varinfo TSH.t
val typeIncl : GoblintCil.fieldinfo TSH.t
val collect_direct_arithmetic : bool 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 Lazy.t -> GoblintCil.exp -> acc_typ
val get_val_type : GoblintCil.exp -> acc_typ
val add_one : side:(Memo.t -> unit) -> Memo.t -> unit

Add access to Memo after distributing.

val add_distribute_outer : side:(Memo.t -> unit) -> side_empty:(Memo.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:(Memo.t -> unit) -> side_empty:(Memo.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 -> 'a) -> GoblintCil.lval -> unit
val distribute_access_lval_addr : (GoblintCil.exp -> 'a) -> GoblintCil.lval -> unit
val distribute_access_offset : (GoblintCil.exp -> 'a) -> GoblintCil.offset -> unit
val distribute_access_exp : (GoblintCil.exp -> 'a) -> GoblintCil.exp -> unit
val distribute_access_type : (GoblintCil.exp -> 'a) -> GoblintCil.typ -> unit
module A : sig ... end
module AS : sig ... end
val may_race : ('a * AccessKind.t * 'b * 'c * MCPAccess.A.t) -> ('d * AccessKind.t * 'e * 'f * MCPAccess.A.t) -> bool
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 ref
val incr_summary : safe:int ref -> vulnerable:int ref -> unsafe:int 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 ref -> vulnerable:int ref -> unsafe:int ref -> WarnAccs.t -> ([< `Type of GoblintCil.typsig & 'a | `Var of CilType.Varinfo.t ] * Offset.Unit.t) -> unit