Spec (goblint.Goblint_lib.ActiveLongjmp.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 event : ('a, 'b, 'c, 'd) Analyses.ctx -> 'e -> 'f -> 'g

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 return : 
  ('a, 'b, 'c, 'd) Analyses.ctx ->
  GoblintCil.exp option ->
  GoblintCil.fundec ->
  'e

val enter : 
  ('a, 'b, 'c, 'd) Analyses.ctx ->
  GoblintCil.lval option ->
  GoblintCil.fundec ->
  GoblintCil.exp list ->
  ('e * 'f) list

val combine_env : 
  'a ->
  GoblintCil.lval option ->
  'b ->
  GoblintCil.fundec ->
  GoblintCil.exp list ->
  'c ->
  'd ->
  Queries.ask ->
  '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 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

val name : unit -> string

module D = JmpBufDomain.ActiveLongjmps

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

val startstate : 'a -> JmpBufDomain.JmpBufSet.t * JmpBufDomain.NodeSet.t

val threadenter : 
  'a ->
  multiple:'b ->
  'c ->
  'd ->
  'e ->
  (JmpBufDomain.JmpBufSet.t * JmpBufDomain.NodeSet.t) list

val exitstate : 'a -> JmpBufDomain.JmpBufSet.t * JmpBufDomain.NodeSet.t

val query : 
  (JmpBufDomain.ActiveLongjmps.t, 'b, 'c, 'd) Analyses.ctx ->
  'a Queries.t ->
  'a0 Queries.result