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

[Frama-c-discuss] kinstr to kernel_function



Well, before posting here, my current solution was somewhat between 1)
and 2). I had the fundec of the function I'm currently visiting and I
was iterating over functions to get the corresponding kf.

Since there is a self#current_stmt method in the visitor, I thought that
maybe a stmt_to_kf method might exist (or maybe fundec_to_kf). It's a
shame I didn't thought of greping for more self#current_* methods :/

> CUOQ Pascal wrote:
>> In fact, either 1) is a lazy solution that I shouldn't even be
>> telling you about because 2) is possible, or there is a big flaw in 
>> our architecture because you were able to paint yourself into a
>> corner where 2) is not possible, in which case we should fix it.

So obvious that it didn't even crossed my mind... thanks a lot for the
tip!
> Virgile Prevosto wrote:
>> the kernel function currently visited is available through the 
>> current_kf method of generic_frama_c_visitor

Well, all the Kernel_function.find_* functions are pretty handy, thanks
for pointing this out.
> SIGNOLES Julien wrote:
>> Using the function Kernel_function.find_from_sid, it should be quite 
>> easy to do what you want.