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. R
    Ralf Vogler
  6. K
    Kalmer Apinis
  7. V
    Vesal Vojdani

Maintainers

  1. S
    Simmo Saan <simmo.saan@gmail.com>
  2. M
    Michael Schwarz <michael.schwarz93@gmail.com>

Sources

goblint-2.2.1.tbz
sha256=ca24f72fa9a87d288affe97c411753f14b7802bab4ca3649b337276b89bf5674
sha512=394b3521ccda0da91540cebb2f433f7525763060be4bbe179edd3b952a3580a8e173c4e410fc6895dc67fe6d17e6699aeddfed600f4692858bec093dd912bf1e

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

Module Goblint_lib.Access

Memory accesses and their manipulation.

module M = Messages
val is_ignorable_type : GoblintCil.typ -> bool
val is_ignorable : (GoblintCil.varinfo * 'a) option -> bool
module TSH : sig ... end
val typeVar : GoblintCil.varinfo TSH.t
val typeIncl : GoblintCil.fieldinfo TSH.t
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_type : GoblintCil.typ Lazy.t -> GoblintCil.exp -> acc_typ
val get_val_type : GoblintCil.exp -> acc_typ
val add_one : side:(Memo.t -> unit) -> Memo.t -> unit

Add access to Memo after distributing.

val add_distribute_outer : side:(Memo.t -> unit) -> side_empty:(Memo.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:(Memo.t -> unit) -> side_empty:(Memo.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 * AccessKind.t * 'b * 'c * MCPAccess.A.t) -> ('d * AccessKind.t * 'e * 'f * MCPAccess.A.t) -> bool
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