--- layout: fc_discuss_archives title: Message 86 from Frama-C-discuss on February 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Kernel functions



Hello Virgile,
> 2012/2/17 Boris Hollas <hollas at informatik.htw-dresden.de>:
> >
> > inherit Visitor.generic_frama_c_visitor prj (Cil.copy_visit ())
> > method vspec s = begin
> >  let new_kf = Cil.get_kernel_function (self#behavior) (Extlib.the
> > self#current_kf) in
> >  Kernel_function.set_spec new_kf (fun _ -> Cil.empty_funspec ());
> >  Cil.DoChildren
> > end
> >

You wrote earlier

> separated). Cil.get_kernel_function (and its twin
> Cil.get_original_kernel_function) allows to retrieve the corresponding
> kf in the new project (and vice-versa).