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 (9)

Authors

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

Maintainers

  1. S
    Simmo Saan <simmo.saan@gmail.com>
  2. M
    Michael Schwarz <michael.schwarz93@gmail.com>
  3. K
    Karoliine Holter <karoliine.holter@ut.ee>

Sources

goblint-2.4.0.tbz
sha256=99b78e6def71534d195eef9084baa26d8334b36084e120aa6afb300c9bf8afa6
sha512=f3162bd95a03c00358a2991f6152fc6169205bfb4c55e2c483e98cc3935673df9656d025b6f1ea0fa5f1bd0aee037d4f483966b0d2907e3fa9bf11a93a3392af

doc/goblint.lib/Goblint_lib/Access/index.html

Module Goblint_lib.Access

Memory accesses and their manipulation.

module M = Messages
val is_ignorable_comp_name : string -> bool
val is_ignorable_attrs : GoblintCil.attribute list -> bool
val is_ignorable_type : GoblintCil.typ -> bool
val is_ignorable_type_offset : GoblintCil.typ -> 'a Offset.t -> bool
val is_ignorable_typsig : GoblintCil.typsig -> bool

is_ignorable_type for typsig.

val is_ignorable_typsig_offset : GoblintCil.typsig -> 'a Offset.t -> bool

is_ignorable_type_offset for typsig.

val is_ignorable_mval : (GoblintCil.varinfo * 'a Offset.t) -> bool
val is_ignorable_memo : ([< `Type of GoblintCil.typsig | `Var of GoblintCil.varinfo ] * 'a Offset.t) -> bool
module TSH : sig ... end
val collect_direct_arithmetic : bool ref
val init : GoblintCil.file -> unit
val reset : unit -> unit
type acc_typ = [
  1. | `Type of CilType.Typ.t
  2. | `Struct of CilType.Compinfo.t * Offset.Unit.t
]

Old access type inferred from an expression.

val equal_acc_typ : acc_typ -> acc_typ -> Ppx_deriving_runtime.bool
val compare_acc_typ : acc_typ -> acc_typ -> Ppx_deriving_runtime.int
val hash_acc_typ : acc_typ -> int
module MemoRoot : sig ... end
module Memo : sig ... end

Memory location of an access.

val get_val_type : GoblintCil.exp -> acc_typ
val add_one : side: ((([< `Type of GoblintCil.typsig | `Var of CilType.Varinfo.t ] as 'a) * Offset.Unit.t) -> unit) -> ('a * Offset.Unit.t) -> unit

Add access to Memo after distributing.

val add_distribute_outer : side: (([ `Type of GoblintCil.typsig | `Var of CilType.Varinfo.t ] * Offset.Unit.t) -> unit) -> side_empty: (([ `Type of GoblintCil.typsig | `Var of CilType.Varinfo.t ] * Offset.Unit.t) -> unit) -> GoblintCil.typsig -> Offset.Unit.t -> unit

Distribute empty access set for type-based access to variables and containing fields. Empty access sets are needed for prefix-type_suffix race checking.

val add : side: (([ `Type of GoblintCil.typsig | `Var of CilType.Varinfo.t ] * Offset.Unit.t) -> unit) -> side_empty: (([ `Type of GoblintCil.typsig | `Var of CilType.Varinfo.t ] * Offset.Unit.t) -> unit) -> CilType.Exp.t -> (CilType.Varinfo.t * CilType.Offset.t) option -> unit

Add access to known variable with offsets or unknown variable from expression.

Distribute to AddrOf of all read lvals in subexpressions.

val distribute_access_lval : (GoblintCil.exp -> 'a) -> GoblintCil.lval -> unit
val distribute_access_lval_addr : (GoblintCil.exp -> 'a) -> GoblintCil.lval -> unit
val distribute_access_offset : (GoblintCil.exp -> 'a) -> GoblintCil.offset -> unit
val distribute_access_exp : (GoblintCil.exp -> 'a) -> GoblintCil.exp -> unit
val distribute_access_type : (GoblintCil.exp -> 'a) -> GoblintCil.typ -> unit
module A : sig ... end
module AS : sig ... end
val may_race : A.t -> A.t -> bool

Check if two accesses may race.

module WarnAccs : sig ... end

Access sets for race detection and warnings.

val group_may_race : WarnAccs.t -> AS.t list
val race_conf : AS.t -> Batteries.Int.t option
val is_all_safe : bool ref
val incr_summary : safe:int ref -> vulnerable:int ref -> unsafe:int ref -> AS.t list -> unit
val print_accesses : ([< `Type of GoblintCil.typsig & 'a | `Var of CilType.Varinfo.t ] * Offset.Unit.t) -> AS.t list -> unit
val warn_global : safe:int ref -> vulnerable:int ref -> unsafe:int ref -> WarnAccs.t -> ([< `Type of GoblintCil.typsig & 'a | `Var of CilType.Varinfo.t ] * Offset.Unit.t) -> unit