Spec (goblint.Goblint_lib.UnassumeAnalysis.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 finalize : unit -> unit

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

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

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

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

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

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 : sig ... end

val startstate : 'a -> D.t

val morphstate : 'a -> 'b -> D.t

val exitstate : 'a -> D.t

module Locator : sig ... end

val location_locator : Locator.t

val loop_locator : Locator.t

type inv = {

}

val invs : inv NH.t

val fun_pres : Cil.exp FH.t

val pre_invs : inv EH.t NH.t

val init : 'a -> unit

val emit_unassume : (D.t, 'a, 'b, 'c) Analyses.ctx -> D.t

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

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

val body : (D.t, 'a, 'b, 'c) Analyses.ctx -> FH.key -> D.t

val asm : (D.t, 'a, 'b, 'c) Analyses.ctx -> D.t

val skip : (D.t, 'a, 'b, 'c) Analyses.ctx -> D.t

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

val enter : ('a, 'b, 'c, 'd) Analyses.ctx -> 'e -> 'f -> 'g -> ('h * D.t) list

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

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