sig
  val datatype : string
  val param : Cil_types.varinfo -> Wp.MemVar.param
  val separation : unit -> Wp.Separation.clause
end