package goblint
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=ca24f72fa9a87d288affe97c411753f14b7802bab4ca3649b337276b89bf5674
sha512=394b3521ccda0da91540cebb2f433f7525763060be4bbe179edd3b952a3580a8e173c4e410fc6895dc67fe6d17e6699aeddfed600f4692858bec093dd912bf1e
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
module P = Analyses.UnitP
val asm : ('a, 'b, 'c, 'd) Analyses.ctx -> 'a
val skip : ('a, 'b, 'c, 'd) Analyses.ctx -> 'a
val paths_as_set : ('a, 'b, 'c, 'd) Analyses.ctx -> 'a list
module A = Analyses.UnitA
module Dom : sig ... end
type t = Dom.t
module D = Dom
module C = Dom
module V : sig ... end
module G : sig ... end
type extra = (GoblintCil.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
module VarH : sig ... end
module VarMap : sig ... end
val add_to_array_map :
GoblintCil.fundec ->
(GoblintCil.varinfo * VD.t) list ->
unit
val attributes_varinfo :
VarMap.key ->
GoblintCil.fundec ->
(GoblintCil.attributes * GoblintCil.attribute list) option
val project_val :
ValueDomainQueries.t ->
(GoblintCil.attributes * GoblintCil.attributes) option ->
PrecisionUtil.int_precision option ->
VD.t ->
bool ->
VD.t
val project :
ValueDomainQueries.t ->
PrecisionUtil.int_precision option ->
CPA.t ->
GoblintCil.fundec ->
CPA.t
val return_var : unit -> AD.t
val heap_var : ('a, 'b, 'c, 'd) Analyses.ctx -> Basetype.Variables.t
val char_array : (GoblintCil.lval, Batteries.bytes) Batteries.Hashtbl.t
val int_returning_binop_FD :
GoblintCil.binop ->
FD.t ->
FD.t ->
IntDomain.IntDomTuple.t
val add_offset_varinfo : Addr.Offs.t -> 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 :
?top:VD.t ->
?full:bool ->
Q.ask ->
glob_fun ->
store ->
address ->
GoblintCil.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 convertToQueryLval :
ValueDomain.AD.Addr.t ->
(GoblintCil.varinfo * GoblintCil.exp Goblint_lib__Offset_intf.t) list
val reachable_top_pointers_types :
(store, G.t, 'a, V.t) Analyses.ctx ->
AD.t ->
Queries.TS.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.
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
.
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 evalbinop_mustbeequal :
Q.ask ->
glob_fun ->
store ->
GoblintCil.binop ->
e1:GoblintCil.exp ->
?t1:GoblintCil.typ ->
e2:GoblintCil.exp ->
?t2:GoblintCil.typ ->
GoblintCil.typ ->
value
Evaluate BinOp using MustBeEqual query as fallback.
val eval_int :
Q.ask ->
glob_fun ->
store ->
GoblintCil.exp ->
IntDomain.IntDomTuple.t
val query_evalint :
Q.ask ->
glob_fun ->
store ->
GoblintCil.exp ->
[> `Bot | `Lifted of IntDomain.IntDomTuple.t | `Top ]
val eval_exp : store -> GoblintCil.exp -> IntDomain.IntDomTuple.int_t option
val eval_funvar :
(store, G.t, 'a, V.t) Analyses.ctx ->
GoblintCil.exp ->
GoblintCil.varinfo list
Evaluate expression as address. Avoids expensive Apron EvalInt if the Int result would be useless to us anyway.
val query_invariant :
(Priv.D.t BaseDomain.basecomponents_t, G.t, 'a, V.t) Analyses.ctx ->
Invariant.context ->
Invariant.t
val query_invariant_global :
('a, [> `Bot | `Lifted1 of Priv.G.t ], 'b, [> `Left of Priv.V.t ])
Analyses.ctx ->
[< `Left of Priv.V.t | `Right of 'c ] ->
Invariant.t
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:GoblintCil.lval ->
?rval_raw:GoblintCil.exp ->
?t_override:GoblintCil.Cil.typ ->
glob_fun ->
store ->
AD.t ->
GoblintCil.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_partitioning :
ValueDomainQueries.t ->
store ->
GoblintCil.varinfo list ->
store
val is_some_bot : value -> bool
module InvariantEval : sig ... end
module Invariant : sig ... end
val invariant :
(InvariantEval.D.t, InvariantEval.G.t, 'a, InvariantEval.V.t) Analyses.ctx ->
Queries.ask ->
(InvariantEval.V.t -> InvariantEval.G.t) ->
InvariantEval.D.t ->
GoblintCil.exp ->
bool ->
InvariantEval.D.t
val assign :
(store, G.t, 'a, V.t) Analyses.ctx ->
GoblintCil.lval ->
GoblintCil.exp ->
store
val branch :
(store, G.t, 'a, V.t) Analyses.ctx ->
GoblintCil.exp ->
bool ->
store
val body : (store, G.t, 'a, V.t) Analyses.ctx -> GoblintCil.fundec -> store
val return :
(store, G.t, 'a, V.t) Analyses.ctx ->
GoblintCil.exp option ->
GoblintCil.fundec ->
store
val vdecl : (store, G.t, 'a, V.t) Analyses.ctx -> GoblintCil.varinfo -> store
val collect_funargs :
Q.ask ->
?warn:bool ->
glob_fun ->
store ->
GoblintCil.exp list ->
address list
From a list of expressions, collect a list of addresses that they might point to, or contain pointers to.
val forkfun :
(D.t, G.t, C.t, V.t) Analyses.ctx ->
GoblintCil.lval option ->
GoblintCil.varinfo ->
GoblintCil.exp list ->
(GoblintCil.lval option * GoblintCil.varinfo * GoblintCil.exp list) list
val assert_fn :
(InvariantEval.D.t, InvariantEval.G.t, 'a, InvariantEval.V.t) Analyses.ctx ->
GoblintCil.exp ->
bool ->
InvariantEval.D.t
val special_unknown_invalidate :
(store, G.t, 'a, V.t) Analyses.ctx ->
'b ->
glob_fun ->
store ->
CilType.Varinfo.t ->
Goblint_lib__LibraryDesc.Cil.Cil.exp list ->
store
val check_invalid_mem_dealloc :
(store, G.t, 'a, V.t) Analyses.ctx ->
GoblintCil.varinfo ->
GoblintCil.exp ->
unit
val combine_env :
(store, G.t, 'a, V.t) Analyses.ctx ->
'b ->
'c ->
GoblintCil.fundec ->
'd ->
'e ->
D.t ->
Queries.ask ->
Priv.D.t Goblint_lib__BaseDomain.basecomponents_t
val threadspawn :
(BaseDomain.BaseComponents(Priv.D).t,
[> `Bot | `Lifted1 of Priv.G.t ],
'a,
[> `Left of Priv.V.t ])
Analyses.ctx ->
GoblintCil.lval option ->
GoblintCil.varinfo ->
GoblintCil.exp list ->
('b, 'c, 'd, 'e) Analyses.ctx ->
D.t
val unassume :
(D.t, G.t, 'a, V.t) Analyses.ctx ->
GoblintCil.exp ->
WideningTokens.TS.elt list ->
D.t
val event :
(store, G.t, 'a, V.t) Analyses.ctx ->
Events.t ->
'b ->
BaseDomain.BaseComponents(Priv.D).t