package goblint

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
include module type of struct include Analyses.IdentitySpec end
include module type of struct include Analyses.DefaultSpec end

Relatively safe default implementations of some boring Spec functions.

module G = Lattice.Unit
module V = Analyses.EmptyV
module P = Analyses.UnitP
type marshal = unit
val init : 'a -> unit
val finalize : unit -> unit
val vdecl : ('a, 'b, 'c, 'd) Analyses.ctx -> 'e -> 'a
val asm : ('a, 'b, 'c, 'd) Analyses.ctx -> 'a
val skip : ('a, 'b, 'c, 'd) Analyses.ctx -> 'a
val query : 'b -> 'a Queries.t -> 'a
val event : ('a, 'b, 'c, 'd) Analyses.ctx -> 'e -> 'f -> 'a
val morphstate : 'a -> 'b -> 'b
val sync : ('a, 'b, 'c, 'd) Analyses.ctx -> 'e -> 'a
val context : 'a -> 'b -> 'c -> 'c
val paths_as_set : ('a, 'b, 'c, 'd) Analyses.ctx -> 'a list
val branch : ('a, 'b, 'c, 'd) Analyses.ctx -> GoblintCil.exp -> bool -> 'a
val body : ('a, 'b, 'c, 'd) Analyses.ctx -> GoblintCil.fundec -> 'a
val return : ('a, 'b, 'c, 'd) Analyses.ctx -> GoblintCil.exp option -> GoblintCil.fundec -> 'a
val enter : ('a, 'b, 'c, 'd) Analyses.ctx -> GoblintCil.lval option -> GoblintCil.fundec -> GoblintCil.exp list -> ('a * 'a) list
module D : sig ... end
include sig ... end
module C : sig ... end
val startcontext : unit -> D.t
val name : unit -> string
val startstate : 'a -> [ `Lifted of SetDomain.Make(CilType.Varinfo).t | `Top ]
val exitstate : 'a -> [ `Lifted of SetDomain.Make(CilType.Varinfo).t | `Top ]
val assign_lval : Queries.ask -> GoblintCil.lval -> [ `Lifted of SetDomain.Make(CilType.Varinfo).t | `Top ] -> [ `Lifted of SetDomain.Make(CilType.Varinfo).t | `Top ]
val assign : ([ `Lifted of SetDomain.Make(CilType.Varinfo).t | `Top ], 'a, 'b, 'c) Analyses.ctx -> GoblintCil.lval -> 'd -> [ `Lifted of SetDomain.Make(CilType.Varinfo).t | `Top ]
val combine_env : ('a, 'b, 'c, 'd) Analyses.ctx -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'a
val combine_assign : ('a, 'b, 'c, 'd) Analyses.ctx -> GoblintCil.lval option -> 'e -> 'f -> 'g -> 'h -> [ `Lifted of SetDomain.Make(CilType.Varinfo).t | `Top ] -> Queries.ask -> [ `Lifted of SetDomain.Make(CilType.Varinfo).t | `Top ]
val special : ([ `Lifted of SetDomain.Make(CilType.Varinfo).t | `Top ], 'a, 'b, 'c) Analyses.ctx -> GoblintCil.lval option -> GoblintCil.Cil.varinfo -> LibraryDesc.Cil.Cil.exp list -> [ `Lifted of SetDomain.Make(CilType.Varinfo).t | `Top ]
val threadenter : 'a -> multiple:'b -> 'c -> 'd -> 'e -> [ `Lifted of SetDomain.Make(CilType.Varinfo).t | `Top ] list
val threadspawn : 'a -> multiple:'b -> 'c -> 'd -> 'e -> 'f -> [ `Lifted of SetDomain.Make(CilType.Varinfo).t | `Top ]
module A : sig ... end
val access : ([ `Lifted of SetDomain.Make(CilType.Varinfo).t | `Top ], 'a, 'b, 'c) Analyses.ctx -> Queries.access -> bool
OCaml

Innovation. Community. Security.