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. V
    Vesal Vojdani
  2. K
    Kalmer Apinis
  3. R
    Ralf Vogler
  4. M
    Michael Schwarz
  5. J
    Julian Erhard
  6. S
    Simmo Saan

Maintainers

  1. M
    Michael Schwarz <michael.schwarz93@gmail.com>
  2. S
    Simmo Saan <simmo.saan@gmail.com>
  3. R
    Ralf Vogler <ralf.vogler@gmail.com>

Sources

goblint-1.1.1.tbz
sha256=999272bfbd3b9b96fcd58987b237ac6e9fa6d92ef935cc89f1ea2b4205185141
sha512=f3bf6ab71cf8c258d3290da4bf9f6fe42d7c671822e0efeb0fc50afdff078ab15e352237e5c1db31c5aa3a9d430691268ed2e5e00da10f2615835f672f91683d

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

Module Base.MainFunctor

Parameters

module Priv : BasePriv.S

Signature

include module type of struct include Analyses.DefaultSpec end
type marshal = unit
val should_join : 'a -> 'b -> bool
val intrpt : ('a, 'b, 'c) Analyses.ctx -> 'a
val asm : ('a, 'b, 'c) Analyses.ctx -> 'a
val skip : ('a, 'b, 'c) Analyses.ctx -> 'a
val morphstate : 'a -> 'b -> 'b
exception Top
module Dom : sig ... end
type t = Dom.t
module G = Priv.G
module D = Dom
module C = Dom
type extra = (Prelude.Ana.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 otherstate : 'a -> store
val exitstate : 'a -> store
val hash : ('a * 'b) -> int
val leq : (CPA.t * 'a) -> (CPA.t * 'b) -> bool
val return_varstore : Prelude.Ana.varinfo Prelude.Ana.ref
val return_varinfo : unit -> Prelude.Ana.varinfo
val return_var : unit -> AD.Addr.t list AD.Map.t
val return_lval : unit -> Prelude.Ana.lval
val heap_var : ('a, 'b, 'c) Analyses.ctx -> Basetype.Variables.t
val init : 'a -> unit
val finalize : unit -> unit
val iDtoIdx : ID.t -> ID.t
val unop_ID : Prelude.Ana.unop -> ID.t -> ID.t
val evalunop : Prelude.Ana.unop -> Cil.typ -> [> `Bot | `Int of ID.t ] -> VD.t
val binop_ID : Cil.ikind -> Prelude.Ana.binop -> ID.t -> ID.t -> ID.t
val add_offset : ([< `Field of 'b * 'a | `Index of 'c * 'a | `NoOffset NoOffset ] as 'a) -> ([> `Field of 'b * 'd | `Index of 'c * 'd ] as 'd) -> 'd
val add_offset_varinfo : Addr.Offs.t -> Addr.t -> Addr.t
val sync' : [ `Init | `Join | `Normal | `Return | `Thread ] -> (BaseDomain.BaseComponents(Priv.D).t, Priv.G.t, 'a) Analyses.ctx -> D.t
val sync : (BaseDomain.BaseComponents(Priv.D).t, Priv.G.t, 'a) Analyses.ctx -> [< `Init | `Join | `Normal | `Return | `Thread ] -> D.t
val publish_all : (BaseDomain.BaseComponents(Priv.D).t, Priv.G.t, 'a) Analyses.ctx -> [ `Init | `Join | `Normal | `Return | `Thread ] -> unit
val get_var : Q.ask -> glob_fun -> store -> Prelude.Ana.varinfo -> value
val get : ?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 get_ptrs : value list -> address list
val reachable_from_value : Q.ask -> glob_fun -> 'a -> value -> Prelude.Ana.typ -> string -> ValueDomain.AD.bucket AD.Map.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 context : Prelude.Ana.fundec -> store -> store
val context_cpa : Prelude.Ana.fundec -> store -> BaseDomain.CPA.t
val convertToQueryLval : ValueDomain.AD.Addr.t -> (CilType.Varinfo.t * ([> `Field of Cil.fieldinfo * 'a | `Index of Prelude.Ana.exp * 'a | `NoOffset ] as 'a)) list
val addrToLvalSet : ValueDomain.AD.Addr.t list AD.Map.t -> Q.LS.t
val reachable_top_pointers_types : (store, G.t, 'a) 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_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 convert_offset : Q.ask -> glob_fun -> store -> Prelude.Ana.offset -> Addr.Offs.t
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 -> ValueDomain.ID.t
val eval_exp : store -> Prelude.Ana.exp -> ValueDomain.ID.int_t option
val eval_funvar : (store, G.t, 'a) Analyses.ctx -> Prelude.Ana.exp -> Prelude.Ana.varinfo list
val eval_rv_address : Q.ask -> glob_fun -> store -> Prelude.Ana.exp -> VD.t

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

val query : (store, G.t, 'b) Analyses.ctx -> 'a Q.t -> 'a Q.result
val update_variable : CPA.key -> Cil.typ -> CPA.value -> CPA.t -> CPA.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, Priv.G.t, 'a) Analyses.ctx option -> ?invariant:bool -> ?lval_raw:Prelude.Ana.lval -> ?rval_raw:Cil.exp -> ?t_override:Cil.typ -> glob_fun -> store -> AD.t -> 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, Priv.G.t, 'a) Analyses.ctx -> Q.ask -> glob_fun -> store -> (AD.t * Cil.typ * value) list -> store
val rem_many : 'a -> store -> Prelude.Ana.varinfo list -> store
val rem_many_paritioning : ValueDomain.Q.ask -> store -> Prelude.Ana.varinfo list -> store
val is_some_bot : [< `Address of 'a AD.Map.t | `Array of ValueDomain.CArrays.t | `Blob of ValueDomain.Blobs.t | `Bot | `Int of ID.t | `List of ValueDomain.Lists.t | `Struct of ValueDomain.Structs.t | `Thread of ValueDomain.Threads.t | `Top | `Union of ValueDomain.Unions.t ] -> bool
val invariant : (store, Priv.G.t, 'a) Analyses.ctx -> Q.ask -> glob_fun -> store -> Prelude.Ana.exp -> bool -> store
val set_savetop : ?ctx:(store, Priv.G.t, 'a) Analyses.ctx -> ?lval_raw:Prelude.Ana.lval -> ?rval_raw:Cil.exp -> Q.ask -> glob_fun -> store -> AD.bucket AD.Map.t -> Prelude.Ana.typ -> VD.t -> store
module Locmap = Deadcode.Locmap
val dead_branches : bool -> bool Deadcode.Locmap.t
val locmap_modify_def : 'a -> Locmap.key -> ('a -> 'a) -> 'a Locmap.t -> unit
val branch : (store, G.t, 'a) Analyses.ctx -> Prelude.Ana.exp -> bool -> store
val body : (store, G.t, 'a) Analyses.ctx -> Prelude.Ana.fundec -> store
val return : (store, G.t, 'a) Analyses.ctx -> Prelude.Ana.exp option -> Prelude.Ana.fundec -> 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 invalidate : ?ctx:(store, Priv.G.t, 'a) Analyses.ctx -> Q.ask -> glob_fun -> store -> Prelude.Ana.exp list -> store
val make_entry : ?thread:bool -> (D.t, G.t, C.t) Analyses.ctx -> Prelude.Ana.fundec -> Prelude.Ana.exp list -> D.t
val enter : (D.t, G.t, C.t) Analyses.ctx -> 'a -> Prelude.Ana.fundec -> Prelude.Ana.exp list -> (D.t * D.t) list
val assert_fn : (store, G.t, 'a) Analyses.ctx -> Prelude.Ana.exp -> bool -> bool -> store
val special_unknown_invalidate : (store, Priv.G.t, 'a) Analyses.ctx -> 'b -> glob_fun -> store -> CilType.Varinfo.t -> Prelude.Ana.exp list -> store
val combine : (store, G.t, 'a) Analyses.ctx -> Prelude.Ana.lval option -> 'b -> Prelude.Ana.fundec -> Prelude.Ana.exp list -> 'c -> D.t -> D.t
val call_descr : Prelude.Ana.fundec -> store -> string
val threadenter : (store, G.t, C.t) Analyses.ctx -> Prelude.Ana.lval option -> Prelude.Ana.varinfo -> Prelude.Ana.exp list -> D.t list
val threadspawn : (D.t, 'a, 'b) Analyses.ctx -> Prelude.Ana.lval option -> Prelude.Ana.varinfo -> Prelude.Ana.exp list -> ('c, 'd, 'e) Analyses.ctx -> D.t