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_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 collect_direct_arithmetic : bool 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_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 -> '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.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 -> 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
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