package goblint

  1. Overview
  2. Docs
Static analysis framework for C

Install 

dune-project
 Dependency

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

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