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

[Frama-c-discuss] RE : kinstr to kernel_function



Hello,

Using the function Kernel_function.find_from_sid, it should be quite easy to do what you want. Somethink like the below code should work but I cannot test it currently.
So sorry in advance for any bug... Nevertheless the idea should be here.

let kf_from_kinstr = function
| Kglobal -> invalid_argument "no kf for this kinstr"
| Kstmt s -> snd (Kernel_function.find_from_sid s.sid)

Module Db groups together functions of plug-ins statically linked with Frama-C, but there are a lot of useful functions available in other modules of the Frama-C kernel. These modules are referenced at top of module Db. One of them is the module Kernel_function.

Best regards,
Julien Signoles


-------- Message d'origine--------
De: frama-c-discuss-bounces at lists.gforge.inria.fr de la part de Jonathan-Christofer Demay
Date: mer. 11/02/2009 18:35
?: frama-c-discuss at lists.gforge.inria.fr
Objet : [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

-------------- section suivante --------------
Une pi?ce jointe non texte a ?t? nettoy?e...
Nom: non disponible
Type: application/ms-tnef
Taille: 3369 octets
Desc: non disponible
Url: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090212/ba44749f/attachment.bin