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