StackTrace.SpecLoc
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
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 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 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 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 D = StackDomain.Dom3
val enter :
(D.t, 'a, 'b, 'c) Analyses.ctx ->
GoblintCil.lval option ->
GoblintCil.fundec ->
GoblintCil.exp list ->
(D.t * D.t) list
val combine_env :
('a, 'b, 'c, 'd) Analyses.ctx ->
'e ->
'f ->
'g ->
'h ->
'i ->
'j ->
'k ->
'l
val startstate : 'a -> CilType.Location.t list
val exitstate : 'a -> CilType.Location.t list
val threadenter :
(D.t, 'a, 'b, 'c) Analyses.ctx ->
multiple:'d ->
'e ->
'f ->
'g ->
D.t list