package goblint

  1. Overview
  2. Docs
package goblint
Legend:
Library
Module
Module type
Parameter
Class
Class type

Parameters

module Priv : BasePriv.S

Signature

include module type of struct include Analyses.DefaultSpec end

Relatively safe default implementations of some boring Spec functions.

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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct