--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on January 2012 ---
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