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.3.0.tbz
sha256=b729c94adb383a39aea32eb005c988dfd44b92af22ee6a4eedf4239542ac6c26
sha512=643b98770e5fe5644324c95c9ae3a9f698f25c8b11b298f0751d524e0b20af368b2a465fc8200b75a73d48fc9a053fd90f5e8920d4db070927f93188bb8687e0

doc/goblint.lib/Goblint_lib/Base/MainFunctor/index.html

Module Base.MainFunctor

Parameters

module Priv : BasePriv.S

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 morphstate : 'a -> 'b -> 'b
val paths_as_set : ('a, 'b, 'c, 'd) Analyses.ctx -> 'a list
module A = Analyses.UnitA
val access : 'a -> 'b -> unit
exception Top
module Dom : sig ... end
type t = Dom.t
module D = Dom
module C = Dom
module V : sig ... end
module G : sig ... end
val priv_getg : ([> `Left of 'a ] -> [> `Bot | `Lifted1 of Priv.G.t ]) -> 'a -> Priv.G.t
val priv_sideg : ([> `Left of 'a ] -> [> `Lifted1 of 'b ] -> 'c) -> 'a -> 'b -> 'c
type extra = (GoblintCil.varinfo * Offs.t * bool) list
type store = D.t
type value = VD.t
type address = AD.t
type glob_fun = V.t -> G.t
type glob_diff = (V.t * G.t) list
val name : unit -> string
val startstate : 'a -> store
val exitstate : 'a -> store
val is_privglob : GoblintCil.varinfo -> bool
module VarH : sig ... end
module VarMap : sig ... end
val array_map : GoblintCil.attributes VarMap.t VarH.t ref
type marshal = GoblintCil.attributes VarMap.t VarH.t
val array_domain_annotation_enabled : bool lazy_t
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_varstore : GoblintCil.varinfo ref
val return_varinfo : unit -> GoblintCil.varinfo
val return_var : unit -> AD.t
val return_lval : unit -> GoblintCil.lval
val longjmp_return : GoblintCil.varinfo ref
val heap_var : bool -> ('a, 'b, 'c, 'd) Analyses.ctx -> Basetype.Variables.t
val char_array : (GoblintCil.lval, Batteries.bytes) Batteries.Hashtbl.t
val init : GoblintCil.attributes VarMap.t VarH.t option -> unit
val finalize : unit -> GoblintCil.attributes VarMap.t VarH.t
val iDtoIdx : ID.t -> ID.t
val unop_ID : GoblintCil.unop -> ID.t -> ID.t
val unop_FD : GoblintCil.unop -> FD.t -> FD.t
val evalunop : GoblintCil.unop -> GoblintCil.Cil.typ -> value -> value
val binop_ID : GoblintCil.Cil.ikind -> GoblintCil.binop -> ID.t -> ID.t -> ID.t
val binop_FD : GoblintCil.Cil.fkind -> GoblintCil.binop -> FD.t -> FD.t -> FD.t
val int_returning_binop_FD : GoblintCil.binop -> FD.t -> FD.t -> IntDomain.IntDomTuple.t
val is_int_returning_binop_FD : GoblintCil.binop -> bool
val evalbinop_base : Q.ask -> store -> GoblintCil.binop -> GoblintCil.typ -> value -> GoblintCil.typ -> value -> GoblintCil.typ -> value
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_var : Q.ask -> glob_fun -> store -> GoblintCil.varinfo -> value
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 get_ptrs : value list -> address list
val reachable_from_value : Q.ask -> glob_fun -> 'a -> value -> GoblintCil.typ -> string -> AD.t
val reachable_from_address : Q.ask -> glob_fun -> store -> address -> address
val reachable_vars : Q.ask -> address list -> glob_fun -> store -> address list
val drop_non_ptrs : CPA.t -> CPA.t
val drop_ints : CPA.t -> CPA.t
val drop_interval : CPA.t -> CPA.t
val drop_intervalSet : CPA.t -> CPA.t
val context : GoblintCil.fundec -> store -> store
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 -> GoblintCil.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 -> GoblintCil.exp -> value

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_back_up : Q.ask -> glob_fun -> store -> GoblintCil.exp -> value
val eval_rv_base : Q.ask -> glob_fun -> store -> GoblintCil.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_rv_base_lval : eval_lv:(Q.ask -> glob_fun -> store -> GoblintCil.lval -> AD.t) -> Q.ask -> glob_fun -> store -> GoblintCil.exp -> GoblintCil.lval -> value
val evalbinop : Q.ask -> glob_fun -> store -> GoblintCil.binop -> e1:GoblintCil.exp -> ?t1:GoblintCil.typ -> e2:GoblintCil.exp -> ?t2:GoblintCil.typ -> GoblintCil.typ -> value
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_fv : Q.ask -> glob_fun -> store -> GoblintCil.exp -> AD.t
val eval_tv : Q.ask -> glob_fun -> store -> GoblintCil.exp -> AD.t
val eval_int : Q.ask -> glob_fun -> store -> GoblintCil.exp -> IntDomain.IntDomTuple.t
val convert_offset : Q.ask -> glob_fun -> store -> GoblintCil.offset -> VD.offs
val eval_lv : Q.ask -> glob_fun -> store -> GoblintCil.lval -> AD.t
val eval_rv_keep_bot : Q.ask -> glob_fun -> store -> GoblintCil.exp -> value
val eval_rv : Q.ask -> glob_fun -> store -> GoblintCil.exp -> value
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 -> ValueDomainQueries.AD.t
val eval_rv_address : Q.ask -> glob_fun -> store -> GoblintCil.exp -> VD.t

Evaluate expression as address. Avoids expensive Apron EvalInt if the Int result would be useless to us anyway.

val is_not_alloc_var : ('a, 'b, 'c, 'd) Analyses.ctx -> GoblintCil.varinfo -> bool
val is_not_heap_alloc_var : ('a, 'b, 'c, 'd) Analyses.ctx -> GoblintCil.varinfo -> bool
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
val query : (store, G.t, 'b, V.t) Analyses.ctx -> 'a Q.t -> 'a Q.result
val update_variable : GoblintCil.varinfo -> GoblintCil.typ -> CPA.value -> CPA.t -> CPA.t
val add_partitioning_dependencies : GoblintCil.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: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 set_many : ctx:(store, G.t, 'a, V.t) Analyses.ctx -> Q.ask -> glob_fun -> store -> (AD.t * GoblintCil.Cil.typ * value) list -> store
val rem_many : 'a -> store -> GoblintCil.varinfo list -> store
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 set_savetop : ctx:(store, G.t, 'a, V.t) Analyses.ctx -> ?lval_raw:GoblintCil.lval -> ?rval_raw:GoblintCil.exp -> Q.ask -> glob_fun -> store -> AD.t -> GoblintCil.typ -> VD.t -> store
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 collect_invalidate : deep:bool -> Q.ask -> ?warn:bool -> glob_fun -> store -> GoblintCil.exp list -> address list
val invalidate : ?deep:bool -> ctx:(store, G.t, 'a, V.t) Analyses.ctx -> Q.ask -> glob_fun -> store -> GoblintCil.exp list -> store
val make_entry : ?thread:bool -> (D.t, G.t, C.t, V.t) Analyses.ctx -> GoblintCil.fundec -> GoblintCil.exp list -> D.t
val enter : (D.t, G.t, C.t, V.t) Analyses.ctx -> 'a -> GoblintCil.fundec -> GoblintCil.exp list -> (D.t * D.t) list
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 * bool
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 points_to_heap_only : ('a, 'b, 'c, 'd) Analyses.ctx -> GoblintCil.exp -> bool
val get_size_of_ptr_target : ('a, 'b, 'c, 'd) Analyses.ctx -> GoblintCil.exp -> ValueDomainQueries.ID.t Queries.result
val special : (store, G.t, C.t, V.t) Analyses.ctx -> GoblintCil.lval option -> GoblintCil.varinfo -> GoblintCil.exp list -> store
val combine_st : (store, G.t, 'a, V.t) Analyses.ctx -> store -> store -> AD.t -> store
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 combine_assign : (store, G.t, 'a, V.t) Analyses.ctx -> GoblintCil.lval option -> 'b -> GoblintCil.fundec -> GoblintCil.exp list -> 'c -> D.t -> Q.ask -> D.t
val threadenter : (D.t, G.t, C.t, V.t) Analyses.ctx -> multiple:'a -> GoblintCil.lval option -> GoblintCil.varinfo -> GoblintCil.exp list -> D.t list
val threadspawn : (BaseDomain.BaseComponents(Priv.D).t, [> `Bot | `Lifted1 of Priv.G.t ], 'a, [> `Left of Priv.V.t ]) Analyses.ctx -> multiple:'b -> GoblintCil.lval option -> GoblintCil.varinfo -> GoblintCil.exp list -> ('c, 'd, 'e, 'f) Analyses.ctx -> D.t
val unassume : (D.t, G.t, 'a, V.t) Analyses.ctx -> GoblintCil.exp -> WideningTokens.TS.elt list -> D.t