package goblint

  1. Overview
  2. Docs
package goblint
Legend:
Library
Module
Module type
Parameter
Class
Class type
include module type of struct include Analyses.IdentitySpec end
include module type of struct include Analyses.DefaultSpec end

Relatively safe default implementations of some boring Spec functions.

module G = Lattice.Unit
module V = Analyses.EmptyV
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 event : ('a, 'b, 'c, 'd) Analyses.ctx -> 'e -> 'f -> 'a
val sync : ('a, 'b, 'c, 'd) Analyses.ctx -> 'e -> 'a
val paths_as_set : ('a, 'b, 'c, 'd) Analyses.ctx -> 'a list
val assign : ('a, 'b, 'c, 'd) Analyses.ctx -> GoblintCil.lval -> GoblintCil.exp -> 'a
val branch : ('a, 'b, 'c, 'd) Analyses.ctx -> GoblintCil.exp -> bool -> 'a
val body : ('a, 'b, 'c, 'd) Analyses.ctx -> GoblintCil.fundec -> 'a
val return : ('a, 'b, 'c, 'd) Analyses.ctx -> GoblintCil.exp option -> GoblintCil.fundec -> 'a
val combine_assign : ('a, 'b, 'c, 'd) Analyses.ctx -> GoblintCil.lval option -> 'e -> GoblintCil.fundec -> GoblintCil.exp list -> 'f -> 'g -> Queries.ask -> 'a
val special : ('a, 'b, 'c, 'd) Analyses.ctx -> GoblintCil.lval option -> GoblintCil.varinfo -> GoblintCil.exp list -> 'a
module N : sig ... end
module TD = Thread.D
module Created : sig ... end
module D : sig ... end

Uniqueness Counter * TID * (All thread creates of current thread * All thread creates of the current function and its callees)

module C = D
module P : sig ... end
val tids : (Thread.t, unit) Batteries.Hashtbl.t Stdlib.ref
val name : unit -> string
val context : 'a -> ('b * 'c * (TD.t * TD.t)) -> 'b * 'c * (TD.t * TD.t)
val startstate : 'a -> [> `Bot ] * [> `Bot ] * (TD.t * TD.t)
val exitstate : GoblintCil.varinfo -> [> `Bot ] * [> `Lifted of Thread.t ] * (TD.t * TD.t)
val morphstate : GoblintCil.varinfo -> 'a -> [> `Bot ] * [> `Lifted of Thread.t ] * (TD.t * TD.t)
val create_tid : ?multiple:bool -> ('a * [> `Lifted of Thread.t ] * (Thread.D.t * 'b)) -> (Node.t * int option) -> GoblintCil.varinfo -> [> `Lifted of Thread.t ] list
val is_unique : ('a, 'b, 'c, 'd) Analyses.ctx -> BoolDomain.MustBool.t Queries.result
val enter : ('a * 'b * ('c * 'd), 'e, 'f, 'g) Analyses.ctx -> 'h -> 'i -> 'j -> (('a * 'b * ('c * 'd)) * ('a * 'b * ('c * TD.t))) list
val combine_env : ('a * 'b * (TD.t * TD.t), 'c, 'd, 'e) Analyses.ctx -> 'f -> 'g -> 'h -> 'i -> 'j -> ('k * 'l * (TD.t * TD.t)) -> 'm -> 'k * 'l * (TD.t * TD.t)
val created : ('a * [> `Lifted of Thread.t ] * (Thread.D.t * 'b)) -> ConcDomain.ThreadSet.t
val query : (D.t, 'b, 'c, 'd) Analyses.ctx -> 'a Queries.t -> 'a Queries.result
module A : sig ... end
val access : ('a * 'b * 'c, 'd, 'e, 'f) Analyses.ctx -> 'g -> 'b option
val indexed_node_for_ctx : ('a, 'b, 'c, 'd) Analyses.ctx -> Node.t * int option

get the node that identifies the current context, possibly that of a wrapper function

val threadenter : ('a * [> `Lifted of Thread.t ] * (Thread.D.t * 'b), 'c, 'd, 'e) Analyses.ctx -> multiple:bool -> 'f -> GoblintCil.varinfo -> 'g -> D.t list
val threadspawn : ('a * 'b * (Thread.D.t * Thread.D.t), 'c, 'd, 'e) Analyses.ctx -> multiple:bool -> 'f -> 'g -> 'h -> ([> `Lifted of GoblintCil.varinfo * Node.t * int option ] * 'i * 'j, 'k, 'l, 'm) Analyses.ctx -> 'a * 'b * (Thread.D.t * Thread.D.t)
type marshal = (Thread.t, unit) Batteries.Hashtbl.t
val init : marshal option -> unit
val print_tid_info : unit -> unit
val finalize : unit -> (Thread.t, unit) Batteries.Hashtbl.t
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