sig exception Not_implemented of string val not_implemented : what:string -> unit val emitter : Emitter.t val assert_and_validate : kf:Kernel_function.t -> Cil_types.stmt -> Cil_types.predicate -> unit end