package goblint

  1. Overview
  2. Docs
package goblint
Legend:
Library
Module
Module type
Parameter
Class
Class type

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 collect_direct_arithmetic : bool Stdlib.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 Stdlib.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 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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct