package goblint
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=dba2b664c7c125687e708e871d83fbfb6ba6d9ee98d235b4850d9a238caa84de
sha512=529987cde39691ad9e955000a3603e89c1c8cf14ed5e8b4cd3a7fc26e47d016aff571b472e2329725133c46f8d0cb45a05b88994eeffaa221a4d31b4c543adcd
doc/goblint.lib/Goblint_lib/Base/MainFunctor/index.html
Module Base.MainFunctor
Parameters
module Priv : BasePriv.S
module RVEval : BaseDomain.ExpEvaluator with type t = BaseComponents(Priv.D).t
Signature
include module type of struct include Analyses.DefaultSpec end
val asm : ('a, 'b, 'c, 'd) Analyses.ctx -> 'a
val skip : ('a, 'b, 'c, 'd) Analyses.ctx -> 'a
module A = Goblint_lib.Analyses.DefaultSpec.A
module Dom : sig ... end
type t = Dom.t
module D = Dom
module C = Dom
module V : sig ... end
module G : sig ... end
type extra = (Prelude.Ana.varinfo * Offs.t * bool) list
type store = D.t
type value = VD.t
type address = AD.t
val startstate : 'a -> store
val exitstate : 'a -> store
val is_privglob : Prelude.Ana.varinfo -> bool
val project_val : PrecisionUtil.int_precision option -> VD.t -> bool -> VD.t
val project : PrecisionUtil.int_precision option -> CPA.t -> CPA.t
val return_varstore : Prelude.Ana.varinfo Prelude.Ana.ref
val return_varinfo : unit -> Prelude.Ana.varinfo
val return_lval : unit -> Prelude.Ana.lval
val heap_var : ('a, 'b, 'c, 'd) Analyses.ctx -> Basetype.Variables.t
val char_array :
(Prelude.Ana.lval, Prelude.Ana.bytes) Goblint_lib.Prelude.Ana.Hashtbl.t
val unop_ID : Prelude.Ana.unop -> ID.t -> ID.t
val unop_FD : Prelude.Ana.unop -> FD.t -> FD.t
val binop_ID :
Goblint_lib.Prelude.Ana.Cil.ikind ->
Prelude.Ana.binop ->
ID.t ->
ID.t ->
ID.t
val binop_FD :
Goblint_lib.Prelude.Ana.Cil.fkind ->
Prelude.Ana.binop ->
FD.t ->
FD.t ->
FD.t
val int_returning_binop_FD :
Prelude.Ana.binop ->
FD.t ->
FD.t ->
IntDomain.IntDomTuple.t
val is_int_returning_binop_FD : Prelude.Ana.binop -> bool
val evalbinop :
Q.ask ->
store ->
Prelude.Ana.binop ->
Prelude.Ana.typ ->
value ->
Prelude.Ana.typ ->
value ->
Prelude.Ana.typ ->
value
val add_offset_varinfo :
(GoblintCil.fieldinfo, IntDomain.IntDomTuple.t) Goblint_lib__Lval.offs ->
Addr.t ->
Addr.t
val sync' :
[ `Init | `Join | `Normal | `Return | `Thread ] ->
(BaseDomain.BaseComponents(Priv.D).t,
[> `Bot | `Lifted1 of Priv.G.t ],
'a,
[> `Left of Priv.V.t ])
Analyses.ctx ->
D.t
val sync :
(BaseDomain.BaseComponents(Priv.D).t,
[> `Bot | `Lifted1 of Priv.G.t ],
'a,
[> `Left of Priv.V.t ])
Analyses.ctx ->
[< `Init | `Join | `Normal | `Return | `Thread ] ->
D.t
val publish_all :
(BaseDomain.BaseComponents(Priv.D).t,
[> `Bot | `Lifted1 of Priv.G.t ],
'a,
[> `Left of Priv.V.t ])
Analyses.ctx ->
[ `Init | `Join | `Normal | `Return | `Thread ] ->
unit
val get_var : Q.ask -> glob_fun -> store -> Prelude.Ana.varinfo -> value
val get :
?top:VD.t ->
?full:bool ->
Q.ask ->
glob_fun ->
store ->
address ->
Prelude.Ana.exp option ->
value
get st addr
returns the value corresponding to addr
in st
* adding proper dependencies. * For the exp argument it is always ok to put None. This means not using precise information about * which part of an array is involved.
val reachable_from_value :
Q.ask ->
glob_fun ->
'a ->
value ->
Prelude.Ana.typ ->
string ->
PreValueDomain.AD.bucket AD.Map.t
val context : Prelude.Ana.fundec -> store -> store
val context_cpa :
Prelude.Ana.fundec ->
store ->
Goblint_lib__MapDomain.LiftTop(ValueDomain.Compound)(MapDomain.HashCached(MapDomain.MapBot(Basetype.Variables)(ValueDomain.Compound))).t
val convertToQueryLval :
Goblint_lib.ValueDomain.AD.Addr.t ->
(CilType.Varinfo.t
* [> `Field of GoblintCil.fieldinfo * 'a
| `Index of Prelude.Ana.exp * 'a
| `NoOffset ] as 'a)
list
val addrToLvalSet : Goblint_lib.ValueDomain.AD.Addr.t list AD.Map.t -> Q.LS.t
val reachable_top_pointers_types :
(store, G.t, 'a, V.t) Analyses.ctx ->
AD.t ->
Queries.TS.t
val eval_rv_ask_evalint : Q.ask -> glob_fun -> store -> Prelude.Ana.exp -> VD.t
Evaluate expression using EvalInt query. Base itself also answers EvalInt, so recursion goes indirectly through queries. This allows every subexpression to also meet more precise value from other analyses. Non-integer expression just delegate to next eval_rv function.
val eval_rv_no_ask_evalint :
Q.ask ->
glob_fun ->
store ->
Prelude.Ana.exp ->
VD.t
Evaluate expression without EvalInt query on outermost expression. This is used by base responding to EvalInt to immediately directly avoid EvalInt query cycle, which would return top. Recursive eval_rv
calls on subexpressions still go through eval_rv_ask_evalint
.
val eval_rv_ask_mustbeequal :
Q.ask ->
glob_fun ->
store ->
Prelude.Ana.exp ->
VD.t
Evaluate expression using MustBeEqual query. Otherwise just delegate to next eval_rv function.
val eval_rv_back_up : Q.ask -> glob_fun -> store -> Prelude.Ana.exp -> value
val eval_rv_base : Q.ask -> glob_fun -> store -> Prelude.Ana.exp -> value
Evaluate expression structurally by base. This handles constants directly and variables using CPA. Subexpressions delegate to eval_rv
, which may use queries on them.
val eval_fv : Q.ask -> glob_fun -> store -> Prelude.Ana.exp -> AD.t
val eval_tv : Q.ask -> glob_fun -> store -> Prelude.Ana.exp -> AD.t
val eval_int :
Q.ask ->
glob_fun ->
store ->
Prelude.Ana.exp ->
Goblint_lib.PreValueDomain.ID.t
val convert_offset :
Q.ask ->
glob_fun ->
store ->
Prelude.Ana.offset ->
(GoblintCil.fieldinfo, IntDomain.IntDomTuple.t) Goblint_lib__Lval.offs
val eval_lv : Q.ask -> glob_fun -> store -> Prelude.Ana.lval -> AD.t
val eval_rv_keep_bot : Q.ask -> glob_fun -> store -> Prelude.Ana.exp -> value
val eval_rv : Q.ask -> glob_fun -> store -> Prelude.Ana.exp -> value
val query_evalint :
Q.ask ->
glob_fun ->
store ->
Prelude.Ana.exp ->
[> `Bot | `Lifted of Goblint_lib.PreValueDomain.ID.t | `Top ]
val eval_exp :
store ->
Prelude.Ana.exp ->
Goblint_lib.ValueDomain.ID.int_t option
val eval_funvar :
(store, G.t, 'a, V.t) Analyses.ctx ->
Prelude.Ana.exp ->
Prelude.Ana.varinfo list
Evaluate expression as address. Avoids expensive Apron EvalInt if the `Int result would be useless to us anyway.
val query_invariant :
('a BaseDomain.basecomponents_t, 'b, 'c, 'd) Analyses.ctx ->
Invariant.context ->
Invariant.t
val add_partitioning_dependencies :
Prelude.Ana.varinfo ->
VD.t ->
store ->
store
Add dependencies between a value and the expression it (or any of its contents) are partitioned by
val set :
Q.ask ->
ctx:(store, G.t, 'a, V.t) Analyses.ctx ->
?invariant:bool ->
?lval_raw:Prelude.Ana.lval ->
?rval_raw:GoblintCil.exp ->
?t_override:Goblint_lib.Prelude.Ana.Cil.typ ->
glob_fun ->
store ->
AD.t ->
Goblint_lib.Prelude.Ana.Cil.typ ->
value ->
store
set st addr val
returns a state where addr
is set to val
* it is always ok to put None for lval_raw and rval_raw, this amounts to not using/maintaining * precise information about arrays.
val rem_many : 'a -> store -> Prelude.Ana.varinfo list -> store
val rem_many_partitioning :
Queries.ask ->
store ->
Prelude.Ana.varinfo list ->
store
val is_some_bot : VD.t -> bool
val invariant_fallback :
(store, G.t, 'a, V.t) Analyses.ctx ->
Q.ask ->
glob_fun ->
store ->
Prelude.Ana.exp ->
bool ->
store
val invariant :
(store, G.t, 'a, V.t) Analyses.ctx ->
Q.ask ->
glob_fun ->
store ->
Prelude.Ana.exp ->
bool ->
store
val set_savetop :
ctx:(store, G.t, 'a, V.t) Analyses.ctx ->
?lval_raw:Prelude.Ana.lval ->
?rval_raw:GoblintCil.exp ->
Q.ask ->
glob_fun ->
store ->
AD.bucket AD.Map.t ->
Prelude.Ana.typ ->
VD.t ->
store
val assign :
(store, G.t, 'a, V.t) Analyses.ctx ->
Prelude.Ana.lval ->
Prelude.Ana.exp ->
store
val branch :
(store, G.t, 'a, V.t) Analyses.ctx ->
Prelude.Ana.exp ->
bool ->
store
val body : (store, G.t, 'a, V.t) Analyses.ctx -> Prelude.Ana.fundec -> store
val return :
(store, G.t, 'a, V.t) Analyses.ctx ->
Prelude.Ana.exp option ->
Prelude.Ana.fundec ->
store
val vdecl : (store, G.t, 'a, V.t) Analyses.ctx -> Prelude.Ana.varinfo -> store
val collect_funargs :
Q.ask ->
?warn:bool ->
glob_fun ->
store ->
Prelude.Ana.exp list ->
address list
From a list of expressions, collect a list of addresses that they might point to, or contain pointers to.
val collect_invalidate :
deep:bool ->
Q.ask ->
?warn:bool ->
glob_fun ->
store ->
Prelude.Ana.exp list ->
address list
val invalidate :
?deep:bool ->
ctx:(store, G.t, 'a, V.t) Analyses.ctx ->
Q.ask ->
glob_fun ->
store ->
Prelude.Ana.exp list ->
store
val make_entry :
?thread:bool ->
(D.t, G.t, C.t, V.t) Analyses.ctx ->
Prelude.Ana.fundec ->
Prelude.Ana.exp list ->
D.t
val enter :
(D.t, G.t, C.t, V.t) Analyses.ctx ->
'a ->
Prelude.Ana.fundec ->
Prelude.Ana.exp list ->
(D.t * D.t) list
val forkfun :
(D.t, G.t, C.t, V.t) Analyses.ctx ->
Prelude.Ana.lval option ->
Prelude.Ana.varinfo ->
Prelude.Ana.exp list ->
(Prelude.Ana.lval option * Prelude.Ana.varinfo * Prelude.Ana.exp list) list
val assert_fn :
(store, G.t, 'a, V.t) Analyses.ctx ->
Prelude.Ana.exp ->
bool ->
store
val special_unknown_invalidate :
(store, G.t, 'a, V.t) Analyses.ctx ->
'b ->
glob_fun ->
store ->
CilType.Varinfo.t ->
Goblint_lib__LibraryDesc.Cil.exp list ->
store
val special :
(store, G.t, C.t, V.t) Analyses.ctx ->
Prelude.Ana.lval option ->
Prelude.Ana.varinfo ->
Prelude.Ana.exp list ->
store
val combine :
(store, G.t, 'a, V.t) Analyses.ctx ->
Prelude.Ana.lval option ->
'b ->
Prelude.Ana.fundec ->
Prelude.Ana.exp list ->
'c ->
D.t ->
D.t
val threadenter :
(D.t, G.t, C.t, V.t) Analyses.ctx ->
Prelude.Ana.lval option ->
Prelude.Ana.varinfo ->
Prelude.Ana.exp list ->
D.t list
val threadspawn :
(D.t, 'a, 'b, 'c) Analyses.ctx ->
Prelude.Ana.lval option ->
Prelude.Ana.varinfo ->
Prelude.Ana.exp list ->
('d, 'e, 'f, 'g) Analyses.ctx ->
D.t
val event :
(store, G.t, 'a, V.t) Analyses.ctx ->
Events.t ->
'b ->
BaseDomain.BaseComponents(Priv.D).t