Module 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 = {
  1. exp : Cil.exp;
  2. uuid : string;
}
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