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 = [

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

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`