Spec (goblint.Goblint

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 asm : ('a, 'b, 'c, 'd) Analyses.man -> 'e

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

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

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

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

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

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

module A = Analyses.UnitA

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

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

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

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

val return : 
  ('a, 'b, 'c, 'd) Analyses.man ->
  GoblintCil.exp option ->
  GoblintCil.fundec ->
  'e

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

val threadspawn : 
  ('a, 'b, 'c, 'd) Analyses.man ->
  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 = BoolDomain.MayBool

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

val combine_env : 
  ('a, 'b, 'c, 'd) Analyses.man ->
  'e ->
  'f ->
  'g ->
  'h ->
  'i ->
  'j ->
  'k ->
  'l

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

val vdecl : (bool, 'a, 'b, 'c) Analyses.man -> GoblintCil.varinfo -> D.t

val startstate : 'a -> D.t

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

val exitstate : 'a -> D.t