package goblint
Module Analyses.IdentitySpec
include module type of struct include DefaultSpec end
module G = DefaultSpec.Gmodule V = DefaultSpec.Vval vdecl : ('a, 'b, 'c, 'd) ctx -> 'e -> 'aval asm : ('a, 'b, 'c, 'd) ctx -> 'aval skip : ('a, 'b, 'c, 'd) ctx -> 'aval query : 'b -> 'a Queries.t -> 'aval event : ('a, 'b, 'c, 'd) ctx -> 'e -> 'f -> 'aval sync : ('a, 'b, 'c, 'd) ctx -> 'e -> 'amodule A = DefaultSpec.Aval assign : ('a, 'b, 'c, 'd) ctx -> GoblintCil.lval -> GoblintCil.exp -> 'aval branch : ('a, 'b, 'c, 'd) ctx -> GoblintCil.exp -> bool -> 'aval body : ('a, 'b, 'c, 'd) ctx -> GoblintCil.fundec -> 'aval return :
('a, 'b, 'c, 'd) ctx ->
GoblintCil.exp option ->
GoblintCil.fundec ->
'aval enter :
('a, 'b, 'c, 'd) ctx ->
GoblintCil.lval option ->
GoblintCil.fundec ->
GoblintCil.exp list ->
('a * 'a) listval special :
('a, 'b, 'c, 'd) ctx ->
GoblintCil.lval option ->
GoblintCil.varinfo ->
GoblintCil.exp list ->
'aval threadenter : ('a, 'b, 'c, 'd) ctx -> 'e -> 'f -> 'g -> 'a listval threadspawn : ('a, 'b, 'c, 'd) ctx -> 'e -> 'f -> 'g -> 'h -> 'a