Module `Access`

module M = Messages

val is_ignorable_type : Cil.typ -> bool

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

module Ident : Printable.S with type t = string

module LabeledString : sig ... end

module LSSet : sig ... end

module LSSSet : sig ... end

module PartAccessResult : sig ... end

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

val typeIncl : (Cil.typsig, CilType.Fieldinfo.t) Batteries.Hashtbl.t

val unsound : bool Batteries.ref

val init : Cil.file -> unit

type offs = [

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

]

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

val remove_idx : Cil.offset -> offs

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

val d_offs : unit -> offs -> 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 d_acct : 
  unit ->
  [< `Struct of Cil.compinfo * offs | `Type of Cil.typ ] ->
  Pretty.doc

val file_re : Str.regexp

val d_loc : unit -> CilType.Location.t -> Pretty.doc

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

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

module HtF (T : Batteries.Hashtbl.HashedType) : sig ... end

module Ht : sig ... end

module Acc_typHashable : Batteries.Hashtbl.HashedType with type t = acc_typ

module TypeHash : sig ... end

module LvalOptHashable : 
  Batteries.Hashtbl.HashedType with type t = (Cil.varinfo * offs) option

module LvalOptHash : sig ... end

module PartOptHashable : 
  Batteries.Hashtbl.HashedType with type t = LSSet.t option

module PartOptHash : sig ... end

val accs : 
  ((int * bool * CilType.Location.t * Cil.exp * LSSet.t) Batteries.Set.t
   * LSSet.t)
    PartOptHash.t
    LvalOptHash.t
    TypeHash.t

type var_o = Cil.varinfo option

type off_o = Cil.offset option

type part = LSSSet.t * LSSet.t

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

val some_accesses : bool Batteries.ref

val add_one : 
  Cil.exp ->
  bool ->
  int ->
  acc_typ ->
  (Cil.varinfo * offs) option ->
  part ->
  unit

val type_from_type_offset : acc_typ -> Cil.typ

val add_struct : 
  Cil.exp ->
  bool ->
  int ->
  acc_typ ->
  (Cil.varinfo * offs) option ->
  part ->
  unit

val add_propagate : Cil.exp -> bool -> int -> acc_typ -> 'a -> part -> unit

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

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

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

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

val add : Cil.exp -> bool -> int -> var_o -> off_o -> part -> unit

val partition_race : 
  'a option ->
  (('b * bool * 'c * 'd * 'e) Batteries.Set.t * LSSet.t) ->
  bool

val only_read : 'a -> (('b * bool * 'c * 'd * 'e) Batteries.Set.t * 'f) -> bool

val common_resource : 'a -> ('b * LSSet.t) -> bool

val bot_partition : 'a option -> 'b -> bool

val check_accs : 
  ('a option * LSSet.t * bool) ->
  ('a * bool * 'b * 'c * LSSet.t) ->
  'a option * LSSet.t * bool

val check_safe : 
  'a option ->
  (('b * bool * 'c * 'd * LSSet.t) Batteries.Set.t * 'e) ->
  'b option ->
  'b option

val is_all_safe : unit -> bool

val print_summary : unit -> unit

val print_accesses : unit -> unit

val print_result : unit -> unit

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/goblint.lib/Access/index.html

Module `Access`

package goblint

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/goblint.lib/Access/index.html

Module Access

dune-project
Dependency

Module `Access`