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] RE : kinstr to kernel_function

  • Subject: [Frama-c-discuss] RE : kinstr to kernel_function
  • From: julien.signoles at (SIGNOLES Julien)
  • Date: Thu, 12 Feb 2009 11:01:38 +0100
  • References: <1234373728.14478.12.camel@supelec>


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 de la part de Jonathan-Christofer Demay
Date: mer. 11/02/2009 18:35
?: frama-c-discuss at
Objet : [Frama-c-discuss] kinstr to kernel_function

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

-------------- 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