sig
  val add_allocates_nothing_funspec : Cil_types.kernel_function -> unit
  class vis_add_loop_allocates : Visitor.frama_c_inplace
  val add_allocates_nothing : unit -> unit
end