package goblint
Static analysis framework for C
Install
Dune Dependency
Authors
Maintainers
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_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 typeVar : GoblintCil.varinfo TSH.t
val typeIncl : GoblintCil.fieldinfo TSH.t
val init : GoblintCil.file -> unit
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 Stdlib.Lazy.t -> GoblintCil.exp -> acc_typ
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
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 incr_summary :
safe:int Stdlib.ref ->
vulnerable:int Stdlib.ref ->
unsafe:int Stdlib.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 Stdlib.ref ->
vulnerable:int Stdlib.ref ->
unsafe:int Stdlib.ref ->
WarnAccs.t ->
([< `Type of GoblintCil.typsig & 'a | `Var of CilType.Varinfo.t ]
* Offset.Unit.t) ->
unit
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>