--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on April 2014 ---
Hi, In pre-processed code, some functions prototype missing formal variables names. Infer_annotation module generate contract for the kernel function without definition, but need the formal variable names to be not missing. How to add variable name for those formal variables of a kernel function. I try to add variable name for those kernel functions, but it can't work. let vi = Kernel_function.get_vi kf in let formals = Cil.getFormalsDecl vi in List.iter (fun f -> if(f.vname = "") f.vname <- "__my_plugin_formal_name" ^ (string_of_int f.vid) ) formals; Thank you very much. -david