--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on April 2011 ---
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>