package goblint

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

May-happen-in-parallel (MHP) domain.

include module type of struct include Printable.Std end

Default dummy definitions.

Include as the first thing to avoid these overriding actual definitions.

val tag : 'a -> 'b
val arbitrary : unit -> 'a
val name : unit -> string
module Pretty = GoblintCil.Pretty
val equal : t -> t -> Ppx_deriving_runtime.bool
val compare : t -> t -> Ppx_deriving_runtime.int
val hash : t -> int
val relift : t -> t
val current : Queries.ask -> t
val pretty : unit -> t -> Pretty.doc
include sig ... end
val show : t -> string
val printXml : 'a BatInnerIO.output -> t -> unit
val to_yojson : t -> [> `String of string ]
val definitely_not_started : (TID.t * ConcDomain.ThreadSet.t) -> TID.t -> bool

Can it be excluded that the thread tid2 is running at a program point where

val exists_definitely_not_started_in_joined : (TID.t * ConcDomain.ThreadSet.t) -> ConcDomain.ThreadSet.t -> bool
val must_be_joined : ConcDomain.ThreadSet.elt -> ConcDomain.ThreadSet.t -> bool

Must the thread with thread id other be already joined

val may_happen_in_parallel : t -> t -> bool

May two program points with respective MHP information happen in parallel

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