Module `Contain.Spec`

include module type of struct include Analyses.DefaultSpec end

type marshal = unit

val should_join : 'a -> 'b -> bool

val call_descr : Cil.fundec -> 'a -> string

val intrpt : ('a, 'b, 'c) Analyses.ctx -> 'a

val vdecl : ('a, 'b, 'c) Analyses.ctx -> 'd -> 'a

val asm : ('a, 'b, 'c) Analyses.ctx -> 'a

val skip : ('a, 'b, 'c) Analyses.ctx -> 'a

val event : ('a, 'b, 'c) Analyses.ctx -> 'd -> 'e -> 'a

val morphstate : 'a -> 'b -> 'b

val context : 'a -> 'b -> 'b

val name : unit -> string

module D : sig ... end

module C = D

module G = ContainDomain.Globals

val add_analyzed_fun : 
  Prelude.Ana.fundec ->
  (string, unit) Prelude.Ana.Hashtbl.t ->
  unit

val init_inh_rel : unit -> unit

val funcount : int Prelude.Ana.ref

val init : 'a -> unit

val is_structor : string -> string -> bool

val is_ext : 
  string ->
  (Cil.varinfo -> 'a * 'b * ContainDomain.ClassNameSet.t) ->
  bool

val entered_funs : (string, int) Prelude.Ana.Hashtbl.t

val translate_field : string -> string -> string

val finalize : unit -> unit

val ignore_this : 
  (ContainDomain.FuncName.t * 'a * 'b) ->
  (Cil.varinfo -> 'c * 'd * ContainDomain.ClassNameSet.t) ->
  bool

val islocal_notmain : 
  string ->
  (Cil.varinfo -> 'a * 'b * ContainDomain.ClassNameSet.t) ->
  bool

val add_reentrant_fun : 
  string ->
  (Cil.varinfo -> 'a * 'b * ContainDomain.ClassNameSet.t) ->
  unit

val is_private : 
  Prelude.Ana.varinfo ->
  (Cil.varinfo -> 'a * 'b * ContainDomain.ClassNameSet.t) ->
  bool

val sync : 
  (D.t, ContainDomain.Globals.t, 'a) Analyses.ctx ->
  'b ->
  ContainDomain.FuncName.t * D.Danger.t * ContainDomain.Diff.t

val time_transfer : string -> (int -> 'a) -> 'a

val danger_bot : ('a * D.Danger.t * 'b, 'c, 'd) Analyses.ctx -> bool

val last_globs : int Prelude.Ana.ref

val repeat : int Prelude.Ana.ref

val last_pp : int Prelude.Ana.ref

val value_size : 'a -> int

val print_progress : Prelude.Ana.fundec -> ('a * 'b * 'c) -> unit

val body : 
  (ContainDomain.FuncName.t * D.Danger.t * ContainDomain.Diff.t,
    'a * 'b * ContainDomain.ClassNameSet.t,
    'c)
    Analyses.ctx ->
  Prelude.Ana.fundec ->
  D.t

val check_vtbl : 
  Prelude.Ana.exp ->
  ('a * D.Danger.t * 'b) ->
  (Cil.varinfo -> 'c * 'd * ContainDomain.ClassNameSet.t) ->
  bool

val get_vtbl : 
  Prelude.Ana.exp ->
  ('a * D.Danger.t * 'b) ->
  (Cil.varinfo -> 'c * 'd * ContainDomain.ClassNameSet.t) ->
  CilType.Varinfo.t list

val zip : 'a list -> 'b list -> ('a * 'b) list

val handle_func_ptr : 
  Prelude.Ana.exp ->
  ('a * D.Danger.t * ContainDomain.Diff.t) ->
  'b ->
  (Cil.varinfo -> 'c * 'd * ContainDomain.ClassNameSet.t) ->
  ('a * D.Danger.t * ContainDomain.Diff.t) * bool

val assign : 
  (D.t, ContainDomain.FieldSet.t * 'a * ContainDomain.ClassNameSet.t, 'b)
    Analyses.ctx ->
  Prelude.Ana.lval ->
  Prelude.Ana.exp ->
  D.t

val branch : 
  (D.t, ContainDomain.FieldSet.t * 'a * ContainDomain.ClassNameSet.t, 'b)
    Analyses.ctx ->
  Prelude.Ana.exp ->
  bool ->
  D.t

val return : 
  (D.t, ContainDomain.FieldSet.t * 'a * ContainDomain.ClassNameSet.t, 'b)
    Analyses.ctx ->
  Prelude.Ana.exp option ->
  Prelude.Ana.fundec ->
  D.t

val eval_funvar : 
  (ContainDomain.FuncName.t * D.Danger.t * 'a,
    'b * ContainDomain.VarNameSet.t * ContainDomain.ClassNameSet.t,
    'c)
    Analyses.ctx ->
  Prelude.Ana.exp ->
  Prelude.Ana.varinfo list

val isBad : 
  ContainDomain.FieldSet.t ->
  'a ->
  'b ->
  ('c * D.Danger.t * 'd, 'e * 'f * ContainDomain.ClassNameSet.t, 'g)
    Analyses.ctx ->
  Prelude.Ana.exp ->
  bool

val query : 
  (ContainDomain.FuncName.t * D.Danger.t * 'b,
    'c * ContainDomain.VarNameSet.t * ContainDomain.ClassNameSet.t,
    'd)
    Analyses.ctx ->
  'a Queries.t ->
  'a Queries.result

val special : 
  (D.t, ContainDomain.FieldSet.t * 'a * ContainDomain.ClassNameSet.t, 'b)
    Analyses.ctx ->
  Prelude.Ana.lval option ->
  Prelude.Ana.varinfo ->
  Prelude.Ana.exp list ->
  D.t

val enter : 
  (D.t, ContainDomain.FieldSet.t * 'a * ContainDomain.ClassNameSet.t, 'b)
    Analyses.ctx ->
  Prelude.Ana.lval option ->
  Prelude.Ana.fundec ->
  Prelude.Ana.exp list ->
  (D.t * D.t) list

val combine : 
  (D.t, ContainDomain.FieldSet.t * 'a * ContainDomain.ClassNameSet.t, 'b)
    Analyses.ctx ->
  Prelude.Ana.lval option ->
  'c ->
  Prelude.Ana.fundec ->
  Prelude.Ana.exp list ->
  'd ->
  D.t ->
  D.t

val startstate : 
  'a ->
  ContainDomain.FuncName.t * D.Danger.t * ContainDomain.Diff.t

val threadenter : 
  'a ->
  'b ->
  'c ->
  'd ->
  (ContainDomain.FuncName.t * D.Danger.t * ContainDomain.Diff.t) list

val threadspawn : ('a, 'b, 'c) Analyses.ctx -> 'd -> 'e -> 'f -> 'g -> 'a

val exitstate : 
  'a ->
  ContainDomain.FuncName.t * D.Danger.t * ContainDomain.Diff.t

Install

Dune Dependency

Authors

Maintainers

Sources

doc/goblint.lib/Contain/Spec/index.html

Module `Contain.Spec`

package goblint

Install

Dune Dependency

Authors

Maintainers

Sources

doc/goblint.lib/Contain/Spec/index.html

Module Contain.Spec

Module `Contain.Spec`