Module `Goblint_lib.Access`

module M = Messages

val is_ignorable_type : GoblintCil.typ -> bool

val is_ignorable : (GoblintCil.varinfo * 'a) option -> bool

val typeVar : (GoblintCil.typsig, GoblintCil.varinfo) Batteries.Hashtbl.t

val typeIncl : (GoblintCil.typsig, GoblintCil.fieldinfo) Batteries.Hashtbl.t

val unsound : bool Batteries.ref

val init : GoblintCil.file -> unit

val reset : unit -> unit

type offs = [

| `NoOffset
| `Index of offs
| `Field of CilType.Fieldinfo.t * offs

]

val equal_offs : offs -> offs -> Ppx_deriving_runtime.bool

val compare_offs : offs -> offs -> Ppx_deriving_runtime.int

val hash_offs : offs -> int

val remove_idx : GoblintCil.offset -> offs

val addOffs : 
  [< `Field of CilType.Fieldinfo.t * 'a | `Index of 'a | `NoOffset ] as 'a ->
  offs ->
  offs

val d_offs : unit -> offs -> GoblintCil.Pretty.doc

type acc_typ = [

| `Type of CilType.Typ.t
| `Struct of CilType.Compinfo.t * offs

]

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

val d_acct : 
  unit ->
  [< `Struct of GoblintCil.compinfo * offs | `Type of GoblintCil.typ ] ->
  GoblintCil.Pretty.doc

val d_memo : 
  unit ->
  ([< `Struct of GoblintCil.compinfo * offs | `Type of GoblintCil.typ ]
   * (GoblintCil.varinfo * offs) option) ->
  GoblintCil.Pretty.doc

val get_type : GoblintCil.typ -> GoblintCil.exp -> acc_typ

type var_o = GoblintCil.varinfo option

type off_o = GoblintCil.offset option

val get_val_type : GoblintCil.exp -> var_o -> off_o -> acc_typ

val add_one : 
  (acc_typ ->
    (GoblintCil.varinfo * offs) option ->
    (int * AccessKind.t * Node.t * GoblintCil.exp * 'a) ->
    unit) ->
  GoblintCil.exp ->
  AccessKind.t ->
  int ->
  acc_typ ->
  (GoblintCil.varinfo * offs) option ->
  'a ->
  unit

val type_from_type_offset : acc_typ -> GoblintCil.typ

val add_struct : 
  (acc_typ ->
    (GoblintCil.varinfo * offs) option ->
    (int * AccessKind.t * Node.t * GoblintCil.exp * 'a) ->
    unit) ->
  GoblintCil.exp ->
  AccessKind.t ->
  int ->
  acc_typ ->
  (GoblintCil.varinfo * offs) option ->
  'a ->
  unit

val add_propagate : 
  (acc_typ ->
    (GoblintCil.varinfo * offs) option ->
    (int * AccessKind.t * Node.t * GoblintCil.exp * 'a) ->
    unit) ->
  GoblintCil.exp ->
  AccessKind.t ->
  int ->
  acc_typ ->
  'b ->
  'a ->
  unit

val distribute_access_lval : 
  ('a -> GoblintCil.exp -> 'b) ->
  'a ->
  GoblintCil.lval ->
  unit

val distribute_access_lval_addr : 
  ('a -> GoblintCil.exp -> 'b) ->
  'a ->
  GoblintCil.lval ->
  unit

val distribute_access_offset : 
  ('a -> GoblintCil.exp -> 'b) ->
  'a ->
  GoblintCil.offset ->
  unit

val distribute_access_exp : 
  ('a -> GoblintCil.exp -> 'b) ->
  'a ->
  GoblintCil.exp ->
  unit

val add : 
  (acc_typ ->
    (GoblintCil.varinfo * offs) option ->
    (int * AccessKind.t * Node.t * GoblintCil.exp * 'a) ->
    unit) ->
  GoblintCil.exp ->
  AccessKind.t ->
  int ->
  var_o ->
  off_o ->
  'a ->
  unit

module A : sig ... end

module AS : sig ... end

module T : sig ... end

module O : sig ... end

module LV : sig ... end

module LVOpt : sig ... end

val may_race : 
  ('a * AccessKind.t * 'b * 'c * MCPAccess.A.t) ->
  ('d * AccessKind.t * 'e * 'f * MCPAccess.A.t) ->
  bool

val group_may_race : AS.t -> AS.t list

val race_conf : AS.t -> Batteries.Int.t option

val is_all_safe : bool Batteries.ref

val incr_summary : 
  int Batteries.ref ->
  int Batteries.ref ->
  int Batteries.ref ->
  ('a * 'b) ->
  AS.t list ->
  unit

val print_accesses : 
  ((GoblintCil.varinfo * offs) option
   * [< `Struct of GoblintCil.compinfo * offs | `Type of GoblintCil.typ ]) ->
  AS.t list ->
  unit

val warn_global : 
  int Batteries.ref ->
  int Batteries.ref ->
  int Batteries.ref ->
  ((GoblintCil.varinfo * offs) option
   * [< `Struct of GoblintCil.compinfo * offs | `Type of GoblintCil.typ ]) ->
  AS.t ->
  unit

Install

Dune Dependency

Authors

Maintainers

Sources

doc/goblint.lib/Goblint_lib/Access/index.html

Module `Goblint_lib.Access`

package goblint

Install

Dune Dependency

Authors

Maintainers

Sources

doc/goblint.lib/Goblint_lib/Access/index.html

Module Goblint_lib.Access

Module `Goblint_lib.Access`