Spec (goblint.Goblint_lib.PoisonVariables.Spec)

include module type of struct include Analyses.IdentityUnitContextsSpec end

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 -> 'f

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

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

val query : 'b -> 'a Queries.t -> 'a0

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

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

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

module A = Analyses.UnitA

val access : 'a -> 'b -> unit

val assign : 
  ('a, 'b, 'c, 'd) Analyses.ctx ->
  GoblintCil.lval ->
  GoblintCil.exp ->
  'e

val branch : ('a, 'b, 'c, 'd) Analyses.ctx -> GoblintCil.exp -> bool -> 'e

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

val combine_assign : 
  ('a, 'b, 'c, 'd) Analyses.ctx ->
  GoblintCil.lval option ->
  'e ->
  GoblintCil.fundec ->
  GoblintCil.exp list ->
  'f ->
  'g ->
  Queries.ask ->
  'h

val special : 
  ('a, 'b, 'c, 'd) Analyses.ctx ->
  GoblintCil.lval option ->
  GoblintCil.varinfo ->
  GoblintCil.exp list ->
  'e

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

module C = Printable.Unit

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

val startcontext : unit -> unit

module VS : sig ... end

val name : unit -> string

module D = VS

val check_mval : VS.t -> ValueDomain.AD.elt -> unit

val rem_mval : VS.t -> ValueDomain.AD.elt -> VS.t

val return : 
  (D.t, 'a, 'b, 'c) Analyses.ctx ->
  GoblintCil.exp option ->
  GoblintCil.fundec ->
  D.t

val enter : 
  (VS.t, 'a, 'b, 'c) Analyses.ctx ->
  GoblintCil.lval option ->
  GoblintCil.fundec ->
  GoblintCil.exp list ->
  (D.t * D.t) list

val combine_env : 
  (VS.t, 'a, 'b, 'c) Analyses.ctx ->
  'd ->
  'e ->
  'f ->
  'g ->
  'h ->
  VS.t ->
  'i ->
  VS.t

val startstate : 'a -> D.t

val threadenter : 'a -> multiple:'b -> 'c -> 'd -> 'e -> D.t list

val exitstate : 'a -> D.t

val event : 
  (D.t, 'a, 'b, 'c) Analyses.ctx ->
  Events.t ->
  (VS.t, 'd, 'e, 'f) Analyses.ctx ->
  D.t