--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on April 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problem with current_func



Hello,

Le jeu. 21 avril 2011 12:50:42 CEST,
zakaria chihani <uaz11 at yahoo.fr> a ?crit :

> We
>  don't understand why, but the execution outs a file with ensures \true 
> on every function (4 functions on the example), and an output that 
> suggests 5 ensure \true clauses (five UNEXPECTED).
> 
> Out of the 4 functions, only 3 are meant to be processed, and the 
> expected pattern is indeed matched 3 times, and creates an ensure clause
>  with the correct cost (49,295 and 1813 : three EXPECTED)
> 
Sorry, I forgot about bug 727 (http://bts.frama-c.com/view.php?id=727)
which is solved in svn, but not in the current release: in Carbon,
current_func is not properly set when inspecting a specification. You
can use self#current_kf instead (which gives you a
Db_types.kernel_function, in fact current_kf should be preferred over
current_func, as a kernel_function contains more information than a
fundec). Note however that current_kf is set also when you're visiting
the specification of a leaf function (prototype without corresponding
implementation). You can discriminate prototypes and definition with
Kernel_function.is_definition.

For what it's worth, the patch against Carbon release that fixes issue
727 is included in this mail.

Best regards,
-- 
Virgile Prevosto
Ing?nieur-Chercheur, CEA, LIST
Laboratoire de S?ret? des Logiciels
+33/0 1 69 08 82 98
-------------- section suivante --------------
Une pi?ce jointe autre que texte a ?t? nettoy?e...
Nom: visitor.patch
Type: text/x-patch
Taille: 3456 octets
Desc: non disponible
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110421/f31c973e/attachment.bin>