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

[Frama-c-discuss] Visitor example in plugin-development guide



On Wed, 2012-01-11 at 10:33 +0100, Virgile Prevosto wrote: 
> > 			(* current_stmt is deprecated, so I changed this to current_kinstr. To extract the Kstmt part, is there a function similar to Extlib.the or do I have to provide my own the_stmt function? *)
> 
> There's currently no function to do that. One might be added in a later 
> version in Cil_datatype.Kinstr (where there is already a 
> kinstr_of_opt_stmt), but anyways, most functions should take a kinstr 
> and not a stmt

but is it alright to use stmt here?

> Actually, since Nitrogen, you have access to the new kernel function, 
> but not to Kernel_function.find_englobing_kf (At this very point, AST 
> has been computed, but not the auxiliary tables necessary to compute 
> this information). The proper way to retrieve the new kf is the following:
> 
> let new_kf = Cil.get_kernel_function (Extlib.the self#current_kf) in
> Queue.add (fun () -> Annotations.add_assert new_kf ...)

shouldn't this be

Cil.get_kernel_function (Cil.copy_visit ()) (Extlib.the self#current_kf)

as the type is

val get_kernel_function : visitor_behavior -> Cil_types.kernel_function-> Cil_types.kernel_function

Also, what does this function do? Does it construct a new kernel function?

-- 
Best regards,
Boris