MallocFresh.Specinclude module type of struct include Analyses.IdentitySpec endinclude module type of struct include Analyses.DefaultSpec endmodule G = Lattice.Unitmodule V = Analyses.EmptyVmodule P = Analyses.EmptyPval vdecl : ('a, 'b, 'c, 'd) Analyses.man -> 'e -> 'aval asm : ('a, 'b, 'c, 'd) Analyses.man -> 'aval skip : ('a, 'b, 'c, 'd) Analyses.man -> 'aval query : 'b -> 'a Queries.t -> 'aval event : ('a, 'b, 'c, 'd) Analyses.man -> 'e -> 'f -> 'aval sync : ('a, 'b, 'c, 'd) Analyses.man -> 'e -> 'aval paths_as_set : ('a, 'b, 'c, 'd) Analyses.man -> 'a listval branch : ('a, 'b, 'c, 'd) Analyses.man -> GoblintCil.exp -> bool -> 'aval body : ('a, 'b, 'c, 'd) Analyses.man -> GoblintCil.fundec -> 'aval return :
('a, 'b, 'c, 'd) Analyses.man ->
GoblintCil.exp option ->
GoblintCil.fundec ->
'aval enter :
('a, 'b, 'c, 'd) Analyses.man ->
GoblintCil.lval option ->
GoblintCil.fundec ->
GoblintCil.exp list ->
('a * 'a) listmodule D : sig ... endval startstate : 'a -> [ `Lifted of SetDomain.Make(CilType.Varinfo).t | `Top ]val exitstate : 'a -> [ `Lifted of SetDomain.Make(CilType.Varinfo).t | `Top ]val assign_lval :
Queries.ask ->
GoblintCil.lval ->
[ `Lifted of SetDomain.Make(CilType.Varinfo).t | `Top ] ->
[ `Lifted of SetDomain.Make(CilType.Varinfo).t | `Top ]val assign :
([ `Lifted of SetDomain.Make(CilType.Varinfo).t | `Top ], 'a, 'b, 'c)
Analyses.man ->
GoblintCil.lval ->
'd ->
[ `Lifted of SetDomain.Make(CilType.Varinfo).t | `Top ]val combine_env :
('a, 'b, 'c, 'd) Analyses.man ->
'e ->
'f ->
'g ->
'h ->
'i ->
'j ->
'k ->
'aval combine_assign :
('a, 'b, 'c, 'd) Analyses.man ->
GoblintCil.lval option ->
'e ->
'f ->
'g ->
'h ->
[ `Lifted of SetDomain.Make(CilType.Varinfo).t | `Top ] ->
Queries.ask ->
[ `Lifted of SetDomain.Make(CilType.Varinfo).t | `Top ]val special :
([ `Lifted of SetDomain.Make(CilType.Varinfo).t | `Top ], 'a, 'b, 'c)
Analyses.man ->
GoblintCil.lval option ->
GoblintCil.Cil.varinfo ->
LibraryDesc.Cil.Cil.exp list ->
[ `Lifted of SetDomain.Make(CilType.Varinfo).t | `Top ]val threadenter :
'a ->
multiple:'b ->
'c ->
'd ->
'e ->
[ `Lifted of SetDomain.Make(CilType.Varinfo).t | `Top ] listval threadspawn :
'a ->
multiple:'b ->
'c ->
'd ->
'e ->
'f ->
[ `Lifted of SetDomain.Make(CilType.Varinfo).t | `Top ]module A : sig ... endval access :
([ `Lifted of SetDomain.Make(CilType.Varinfo).t | `Top ], 'a, 'b, 'c)
Analyses.man ->
Queries.access ->
bool