MainFunctor (p.goblint.2.3.0.doc.goblint.lib.Goblint

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 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 : 
  (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

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 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 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 ->
  GoblintCil.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

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