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

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

module V = Basetype.Variables

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 char_array : (Prelude.Ana.lval, Prelude.Ana.bytes) Prelude.Ana.Hashtbl.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 evalbinop : 
  Q.ask ->
  store ->
  Prelude.Ana.binop ->
  Prelude.Ana.typ ->
  value ->
  Prelude.Ana.typ ->
  value ->
  Prelude.Ana.typ ->
  value

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 eval_int : 
  Q.ask ->
  glob_fun ->
  store ->
  Prelude.Ana.exp ->
  ValueDomain.ID.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

val assign : 
  (store, G.t, 'a) Analyses.ctx ->
  Prelude.Ana.lval ->
  Prelude.Ana.exp ->
  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 vdecl : (store, G.t, 'a) 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 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 forkfun : 
  (D.t, G.t, C.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) 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 special : 
  (store, G.t, C.t) Analyses.ctx ->
  Prelude.Ana.lval option ->
  Prelude.Ana.varinfo ->
  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

val event : 
  (store, G.t, 'a) Analyses.ctx ->
  Events.t ->
  ('b, Priv.G.t, 'c) Analyses.ctx ->
  BaseDomain.BaseComponents(Priv.D).t

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module `Base.MainFunctor`

Parameters

Signature

package goblint

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module Base.MainFunctor

Parameters

Signature

Module `Base.MainFunctor`