--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on April 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] add variable name for formal variables of a kernel function



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