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