package goblint

You can search for identifiers within the package.

in-package search v0.2.0

Static analysis framework for C

Install

dune-project

Dependency

goblint.in.tum.de Edit opam file Versions (11)

Authors

Maintainers

Sources

goblint-2.8.0.tbz

sha256=9175eec0143102243964e34a0786584fd590c60422009259c705a89a27f88de4

sha512=9d760007dd8d003cf596516444ed7acc7370fc3d446e75ac71b0176522c3baae090410762f9035e7aae4f6b0e394bf28bb5b1c08ca0476920b94aa919ef04f42

doc/goblint.lib/Goblint_lib/CreationLockset/Spec/A/index.html

Module `Spec.A`

ego tid * must-lockset * creation-lockset

include sig ... end

type t = TID.t * Lockset.t * G.t

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 tag : 'a -> 'b

val arbitrary : unit -> (TID.t * Lockset.t * G.t) QCheck.arbitrary

val name : unit -> string

val one_protected_inter_threaded_other_intra_threaded : 
  G.t ->
  TID.t ->
  G.value ->
  bool

checks if cl1 has a mapping (tp1 |-> ls1) such that ls1 and ls2 are not disjoint and tp1 != t2

parameter cl1
creation-lockset of thread t1 at first program point

parameter t2
thread id at second program point

parameter ls2
lockset at second program point

returns
whether t1 must be running mutually exclusive with second program point

val both_protected_inter_threaded : G.t -> G.t -> bool

checks if cl1 has a member (tp1 |-> ls1) and cl2 has a member (tp2 |-> ls2) such that ls1 and ls2 are not disjoint and tp1 != tp2

parameter cl1
creation-lockset of first thread t1

parameter cl2
creation-lockset of second thread t2

returns
whether t1 and t2 must be running mutually exclusive

val may_race : (TID.t * G.value * G.t) -> (TID.t * G.value * G.t) -> bool

val pretty : unit -> ('a * 'b * G.t) -> Printable.Pretty.doc

val show : ('a * 'b * G.t) -> string

val to_yojson : ('a * 'b * G.t) -> Yojson.Safe.t

val printXml : 'a BatInnerIO.output -> ('b * 'c * G.t) -> unit

val should_print : ('a * 'b * G.t) -> bool