Frama-C-discuss mailing list archives

Pascal.CUOQ at cea.fr (CUOQ Pascal) · Wed, 11 Feb 2009 23:09:30 +0100

Considering the architecture of Frama-C, if such a function existed, it would definitely have to be referenced in kernel/db.mli. 
There is no such function there, and greping for "kinstr" shows that quite often a kinstr is manipulated alongside
 the kernel_function it corresponds to, confirming that the function that you need does not exist. 

You have two ways to go:
1) write the fifteen lines of code that iterate over functions, and for each function over the kinstrs of this function.
Build a huge hashtable from kinstr to kernel_function along the way.
Call these 15 lines an analysis, and make this analysis record its results in Db.
2) there must be a point in the code you are writing where you know the kernel_function your kinstr belongs to.
Transmit this information to the point where you need it.

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.

Pascal

-----Original Message-----
From: frama-c-discuss-bounces at lists.gforge.inria.fr on behalf of Jonathan-Christofer Demay
Sent: Wed 2/11/2009 6:35 PM
To: frama-c-discuss at lists.gforge.inria.fr
Subject: [Frama-c-discuss] kinstr to kernel_function

Hi,

Does anyone know if there's a way to get the Db_types.kernel_function to
which a particular Cil_types.kinstr belongs ?

Thanks in advance for any tip ^^

_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss