sig
type param =
NotUsed
| ByAddr
| ByValue
| ByShift
| ByRef
| InContext
| InArray
val pp_param : Format.formatter -> Wp.Separation.param -> unit
type partition
type clause
val empty : Wp.Separation.partition
val set :
Cil_types.varinfo ->
Wp.Separation.param -> Wp.Separation.partition -> Wp.Separation.partition
val requires : Wp.Separation.partition -> Wp.Separation.clause
val is_true : Wp.Separation.clause -> bool
val filter : Wp.Separation.clause list -> Wp.Separation.clause list
val pp_clause : Format.formatter -> Wp.Separation.clause -> unit
end