package goblint

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

Data race analyzer without base --- this is the new standard

include module type of struct include UnitAnalysis.Spec end
include module type of struct include Analyses.DefaultSpec end

Relatively safe default implementations of some boring Spec functions.

module P = Analyses.UnitP
type marshal = unit
val vdecl : ('a, 'b, 'c, 'd) Analyses.ctx -> 'e -> 'a
val asm : ('a, 'b, 'c, 'd) Analyses.ctx -> 'a
val skip : ('a, 'b, 'c, 'd) Analyses.ctx -> 'a
val morphstate : 'a -> 'b -> 'b
val sync : ('a, 'b, 'c, 'd) Analyses.ctx -> 'e -> 'a
val context : 'a -> 'b -> 'b
val paths_as_set : ('a, 'b, 'c, 'd) Analyses.ctx -> 'a list
module A = Analyses.UnitA
val access : 'a -> 'b -> unit
module D = Lattice.Unit
module C = Lattice.Unit
val assign : (D.t, 'a, 'b, 'c) Analyses.ctx -> GoblintCil.lval -> GoblintCil.exp -> D.t
val branch : (D.t, 'a, 'b, 'c) Analyses.ctx -> GoblintCil.exp -> bool -> D.t
val body : (D.t, 'a, 'b, 'c) Analyses.ctx -> GoblintCil.fundec -> D.t
val return : (D.t, 'a, 'b, 'c) Analyses.ctx -> GoblintCil.exp option -> GoblintCil.fundec -> D.t
val enter : (D.t, 'a, 'b, 'c) Analyses.ctx -> GoblintCil.lval option -> GoblintCil.fundec -> GoblintCil.exp list -> (D.t * D.t) list
val combine_env : 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'g
val combine_assign : (D.t, 'a, 'b, 'c) Analyses.ctx -> GoblintCil.lval option -> 'd -> GoblintCil.fundec -> GoblintCil.exp list -> 'e -> D.t -> Queries.ask -> D.t
val startstate : 'a -> unit
val threadenter : 'a -> 'b -> 'c -> 'd -> unit list
val threadspawn : ('a, 'b, 'c, 'd) Analyses.ctx -> 'e -> 'f -> 'g -> 'h -> 'a
val exitstate : 'a -> unit
val name : unit -> string
module V : sig ... end
module MemoSet : sig ... end
module OneOffset : sig ... end
module OffsetTrie : sig ... end
module G : sig ... end
val safe : int Stdlib.ref
val vulnerable : int Stdlib.ref
val unsafe : int Stdlib.ref
val init : 'a -> unit
val side_vars : ('a, [> `Lifted2 of MemoSet.t ], 'b, [> `Right of CilType.Varinfo.t ]) Analyses.ctx -> MemoSet.elt -> unit
val side_access : ('a, [> `Lifted1 of OffsetTrie.t | `Lifted2 of MemoSet.t ], 'b, [> `Left of [ `Var of CilType.Varinfo.t | `Type of CilType.Typsig.t ] | `Right of CilType.Varinfo.t ]) Analyses.ctx -> (int * AccessKind.t * Node.t * CilType.Exp.t * MCPAccess.A.t) -> ([ `Var of CilType.Varinfo.t | `Type of CilType.Typsig.t ] * Offset.Unit.t) -> unit
val side_access_empty : ('a, [> `Lifted1 of OffsetTrie.t | `Lifted2 of MemoSet.t ], 'b, [> `Left of [ `Var of CilType.Varinfo.t | `Type of CilType.Typsig.t ] | `Right of CilType.Varinfo.t ]) Analyses.ctx -> ([ `Var of CilType.Varinfo.t | `Type of CilType.Typsig.t ] * Offset.Unit.t) -> unit

Side-effect empty access set for prefix-type_suffix race checking.

val type_suffix_memo : Access.Memo.t -> Access.Memo.t option

Get immediate type_suffix memo.

val find_type_suffix' : ('a, [> `Bot | `Lifted1 of OffsetTrie.t ], 'b, [> `Left of [ `Var of CilType.Varinfo.t | `Type of CilType.Typsig.t ] ]) Analyses.ctx -> Access.Memo.t -> Access.AS.t
val find_type_suffix : ('a, [> `Bot | `Lifted1 of OffsetTrie.t ], 'b, [> `Left of [ `Var of CilType.Varinfo.t | `Type of CilType.Typsig.t ] ]) Analyses.ctx -> Access.Memo.t -> Access.AS.t

Find accesses from all type_suffixes transitively.

val query : ('b, [> `Bot | `Lifted1 of OffsetTrie.t | `Lifted2 of MemoSet.t ], 'c, V.t) Analyses.ctx -> 'a Queries.t -> 'a Queries.result
val event : ('a, 'b, 'c, 'd) Analyses.ctx -> Events.t -> ('e, [> `Lifted1 of OffsetTrie.t | `Lifted2 of MemoSet.t ], 'f, [> `Left of [ `Var of CilType.Varinfo.t | `Type of CilType.Typsig.t ] | `Right of CilType.Varinfo.t ]) Analyses.ctx -> 'a
val special : (D.t, [> `Lifted1 of OffsetTrie.t | `Lifted2 of MemoSet.t ], 'a, [> `Left of [ `Var of CilType.Varinfo.t | `Type of CilType.Typsig.t ] | `Right of CilType.Varinfo.t ]) Analyses.ctx -> GoblintCil.lval option -> GoblintCil.varinfo -> GoblintCil.exp list -> D.t
val finalize : unit -> 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