Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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