package goblint

  1. Overview
  2. Docs
package goblint
Legend:
Library
Module
Module type
Parameter
Class
Class type
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 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
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 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 isBad : ContainDomain.FieldSet.t -> 'a -> 'b -> ('c * D.Danger.t * 'd, 'e * 'f * ContainDomain.ClassNameSet.t, 'g) Analyses.ctx -> Prelude.Ana.exp -> bool
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