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