package goblint

  1. Overview
  2. Docs
Static analysis framework for C

Install

Dune Dependency

goblint.in.tum.de Readme Changelog Edit opam file Versions (8)

Authors

  1. V
    Vesal Vojdani
  2. K
    Kalmer Apinis
  3. R
    Ralf Vogler
  4. M
    Michael Schwarz
  5. J
    Julian Erhard
  6. S
    Simmo Saan

Maintainers

  1. M
    Michael Schwarz <michael.schwarz93@gmail.com>
  2. S
    Simmo Saan <simmo.saan@gmail.com>
  3. R
    Ralf Vogler <ralf.vogler@gmail.com>

Sources

goblint-1.1.1.tbz
sha256=999272bfbd3b9b96fcd58987b237ac6e9fa6d92ef935cc89f1ea2b4205185141
sha512=f3bf6ab71cf8c258d3290da4bf9f6fe42d7c671822e0efeb0fc50afdff078ab15e352237e5c1db31c5aa3a9d430691268ed2e5e00da10f2615835f672f91683d

doc/goblint.lib/Osek/Spec/index.html

Module Osek.Spec

include module type of struct include Analyses.DefaultSpec end
type marshal = unit
val call_descr : Cil.fundec -> 'a -> string
val vdecl : ('a, 'b, 'c) Analyses.ctx -> 'd -> 'a
val asm : ('a, 'b, 'c) Analyses.ctx -> 'a
val skip : ('a, 'b, 'c) Analyses.ctx -> 'a
val event : ('a, 'b, 'c) Analyses.ctx -> 'd -> 'e -> 'a
val morphstate : 'a -> 'b -> 'b
val sync : ('a, 'b, 'c) Analyses.ctx -> 'd -> 'a
val context : 'a -> 'b -> 'b
val names : (LockDomain.Addr.t * 'a) -> string
val resourceset_to_priority : string list -> int
val listrem : 'a -> 'a list -> 'a list
val proj3_1 : ('a * 'b * 'c) -> 'a
val proj3_2 : ('a * 'b * 'c) -> 'b
val proj3_3 : ('a * 'b * 'c) -> 'c
val proj2_1 : ('a * 'b) -> 'a
val proj2_2 : ('a * 'b) -> 'b
val parse_oil : unit -> unit
val parse_names : string -> unit
val parse_ids : string -> unit
module MyParam : sig ... end
module M : sig ... end
module Offs = ValueDomain.Offs
module Lockset = LockDomain.Lockset
module Flags = FlagModes.Spec.D
module Acc : sig ... end
module AccKeySet : sig ... end
module AccLoc : sig ... end
module AccValSet : sig ... end
val acc : AccValSet.t Acc.t
module D = M.D
module C = M.C
module G = M.G
val offensivepriorities : (string, int) Prelude.Ana.Hashtbl.t
val off_pry_with_flag : (string, (Flags.t * int) list) Prelude.Ana.Hashtbl.t
val dummy_release : Prelude.Ana.fundec -> Cil.varinfo
val dummy_get : Prelude.Ana.fundec -> Cil.varinfo
val is_task_res' : (LockDomain.Addr.t * 'a) -> bool
val lockset_to_task : D.ReverseAddrSet.t -> string
val mem : Prelude.Ana.exp -> D.ReverseAddrSet.t -> bool
val strip_tags : [> `Lifted of 'a ] -> 'a
val get_eq : Flags.key -> ('a * Flags.t) -> bool
val get_method : Flags.key -> ('a * Flags.t) -> bool
val flag_unknown : Flags.key -> ('a * Flags.t) -> bool
val flag_top : Flags.key -> ('a * Flags.t) -> bool
val flag_list_to_string : Prelude.Ana.varinfo list -> string
val filter_bot : Flags.key -> ('a * Flags.t) list -> ('a * Flags.t) list
val split_accs_top : Flags.key -> ('a * Flags.t) list -> ('a * Flags.t) list * ('a * Flags.t) list
val split_accs_method : Flags.key -> ('a * Flags.t) list -> ('a * Flags.t) list * ('a * Flags.t) list
val split_accs : Flags.key -> ('a * Flags.t) list -> ('a * Flags.t) list * ('a * Flags.t) list
val split_equals : Flags.key -> ('a * Flags.t) list -> ('a * Flags.t) list list
val split_may_eq : Flags.key -> IntDomain.FlatPureIntegers.t -> ('a * Flags.t) list -> ('a * Flags.t) list
val strip_flags : ('a * 'b) list -> 'a list
val get_flags : (string * Obj.t) list -> Flags.t
val just_locks : ('a * Lockset.ReverseAddrSet.t * 'b) list -> Lockset.ReverseAddrSet.elt list list
val prys : ('a * Lockset.ReverseAddrSet.t * 'b) list -> string list list
val staticprys : string list list -> string list list
val offprys : ('a * Lockset.ReverseAddrSet.t * 'b) list -> int list
val accprys : ('a * Lockset.ReverseAddrSet.t * 'b) list -> int list
val maxpry : ('a * Lockset.ReverseAddrSet.t * 'b) list -> int
val minpry : ('a * Lockset.ReverseAddrSet.t * 'b) list -> int
val offpry : ('a * Lockset.ReverseAddrSet.t * 'b) list -> int
val minoffpry : ('a * Lockset.ReverseAddrSet.t * 'b) list -> int
val offpry_flags : Flags.t -> Cil.varinfo -> int
val query_lv : Queries.ask -> Cil.exp -> Queries.LS.elt list
val eval_fv : Queries.ask -> Cil.exp -> CilType.Varinfo.t option
val eval_arg : ('a, 'b, 'c) Analyses.ctx -> Prelude.Ana.exp -> Prelude.Ana.varinfo
val add_concrete_access : ('a, [> `Bot | `Lifted of int64 ], 'b) Analyses.ctx -> Flag.t -> CilType.Location.t -> Lockset.t -> Flags.t -> (Cil.varinfo * Offs.t * bool) -> unit
val add_per_element_access : 'a -> 'b -> 'c -> 'd -> bool
val type_inv_tbl : (int, CilType.Varinfo.t) Prelude.Ana.Hashtbl.t
val type_inv : Prelude.Ana.compinfo -> Lval.CilLval.t list
val best_type_inv : Cil.exp list -> (Prelude.Ana.varinfo * Offs.t) option
val unknown_access : unit -> unit
val add_type_access : ('a, [> `Bot | `Lifted of int64 ], 'b) Analyses.ctx -> Flag.t -> CilType.Location.t -> Lockset.t -> Flags.t -> (Prelude.Ana.exp * bool) -> unit
type access =
  1. | Concrete of Prelude.Ana.exp option * Prelude.Ana.varinfo * Offs.t * bool
  2. | Region of Prelude.Ana.exp option * Prelude.Ana.varinfo * Offs.t * bool
  3. | Unknown of Prelude.Ana.exp * bool
type accesses = access list
val struct_type_inv : Prelude.Ana.varinfo -> Offs.t -> (Prelude.Ana.varinfo * Offs.t) option
val add_accesses : ('a, [> `Bot | `Lifted of int64 ], 'b) Analyses.ctx -> accesses -> Flags.t -> D.t -> unit
val conv_offset : [< `Field of 'b * 'a | `Index of Prelude.Ana.exp * 'a | `NoOffset ] as 'a -> [> `Field of 'b * 'c | `Index of ValueDomain.IndexDomain.t * 'c | `NoOffset ] as 'c
val conv_const_offset : Prelude.Ana.offset -> [> `Field of Prelude.Ana.fieldinfo * 'a | `Index of ValueDomain.IndexDomain.t * 'a | `NoOffset ] as 'a
val replace_elem : ('a * [< `Field of 'c * 'b | `Index of Prelude.Ana.exp * 'b | `NoOffset ] as 'b) -> Prelude.Ana.exp -> Prelude.Ana.exp -> 'a * [> `Field of 'c * 'd | `Index of ValueDomain.IndexDomain.t * 'd | `NoOffset ] as 'd
val access_address : Queries.ask -> (Prelude.Ana.varinfo * [< `Field of Cil.fieldinfo * 'a | `Index of Prelude.Ana.exp * 'a | `NoOffset ] as 'a) list -> bool -> Cil.lval -> accesses
val access_one_byval : Queries.ask -> bool -> Prelude.Ana.exp -> accesses
val access_lv_byval : Queries.ask -> Prelude.Ana.lval -> accesses
val access_one_top : Queries.ask -> bool -> Prelude.Ana.exp -> accesses
val access_byval : Queries.ask -> bool -> Prelude.Ana.exp list -> accesses
val access_reachable : (Queries.LS.t Queries.t -> Queries.LS.t) -> Prelude.Ana.exp list -> access list
val startstate : 'a -> D.ReverseAddrSet.t
val exitstate : 'a -> D.ReverseAddrSet.t
val threadenter : 'a -> 'b -> 'c -> 'd -> D.ReverseAddrSet.t list
val threadspawn : ('a, 'b, 'c) Analyses.ctx -> 'd -> 'e -> 'f -> 'g -> 'a
val activate_task : ('a, 'b, 'c) Analyses.ctx -> string -> unit
val intrpt : (D.t, 'a, 'b) Analyses.ctx -> D.t
val assign : (D.t, [> `Bot | `Lifted of int64 ], 'a) Analyses.ctx -> Prelude.Ana.lval -> Prelude.Ana.exp -> D.t
val branch : (D.t, [> `Bot | `Lifted of int64 ], 'a) Analyses.ctx -> Prelude.Ana.exp -> bool -> D.t
val body : (M.D.t, M.G.t, M.C.t) Analyses.ctx -> Prelude.Ana.fundec -> D.t
val eval_funvar : (Flags.t, [> `Bot | `Lifted of int64 ], 'a) Analyses.ctx -> Prelude.Ana.exp -> D.t -> unit
val enter : (M.D.t, 'a, 'b) Analyses.ctx -> Prelude.Ana.lval option -> Prelude.Ana.fundec -> Prelude.Ana.exp list -> (D.t * D.t) list
val name : unit -> string
val es_to_string : Prelude.Ana.fundec -> 'a -> string
val should_join : D.t -> D.t -> bool

Finalization and other result printing functions:

val race_free : bool Prelude.Ana.ref

are we still race free

type access_status =
  1. | Race
  2. | Guarded of Mutex.Lockset.t
  3. | Priority of int
  4. | Defence of int * int
  5. | Flag of string
  6. | ReadOnly
  7. | ThreadLocal
  8. | HighRead
  9. | HighWrite
  10. | LowRead
  11. | LowWrite
  12. | BadFlag
  13. | GoodFlag
  14. | SomeFlag of int
module OffsMap : sig ... end

modules used for grouping varinfos by Offset

module OffsSet : sig ... end
val suppressed : int Prelude.Ana.ref
val filtered : int Prelude.Ana.ref
val postprocess_acc : Prelude.Ana.varinfo -> unit

postprocess_acc gl groups and report races in gl

val finalize : unit -> unit

postprocess and print races and other output

val init : 'a -> 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