Access (goblint.Goblint

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 Stdlib.ref

val init : GoblintCil.file -> unit

val reset : unit -> unit

type acc_typ = [

| `Type of CilType.Typ.t
| `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 -> int option

val is_all_safe : bool Stdlib.ref

val incr_summary : 
  safe:int Stdlib.ref ->
  vulnerable:int Stdlib.ref ->
  unsafe:int Stdlib.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 Stdlib.ref ->
  vulnerable:int Stdlib.ref ->
  unsafe:int Stdlib.ref ->
  WarnAccs.t ->
  ([< `Type of GoblintCil.typsig & 'a | `Var of CilType.Varinfo.t ]
   * Offset.Unit.t) ->
  unit