package goblint
Module Analyses.IdentitySpec
include module type of struct include DefaultSpec end
val intrpt : ('a, 'b, 'c) ctx -> 'aval vdecl : ('a, 'b, 'c) ctx -> 'd -> 'aval asm : ('a, 'b, 'c) ctx -> 'aval skip : ('a, 'b, 'c) ctx -> 'aval query : 'b -> 'a Queries.t -> 'a Queries.resultval event : ('a, 'b, 'c) ctx -> 'd -> 'e -> 'aval sync : ('a, 'b, 'c) ctx -> 'd -> 'aval assign : ('a, 'b, 'c) ctx -> Cil.lval -> Cil.exp -> 'aval branch : ('a, 'b, 'c) ctx -> Cil.exp -> bool -> 'aval body : ('a, 'b, 'c) ctx -> Cil.fundec -> 'aval return : ('a, 'b, 'c) ctx -> Cil.exp option -> Cil.fundec -> 'aval enter :
('a, 'b, 'c) ctx ->
Cil.lval option ->
Cil.fundec ->
Cil.exp list ->
('a * 'a) listval special :
('a, 'b, 'c) ctx ->
Cil.lval option ->
Cil.varinfo ->
Cil.exp list ->
'aval threadenter : ('a, 'b, 'c) ctx -> 'd -> 'e -> 'f -> 'a listval threadspawn : ('a, 'b, 'c) ctx -> 'd -> 'e -> 'f -> 'g -> 'a