--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on April 2011 ---
Le lun. 11 avril 2011 10:46:38 CEST, zakaria chihani <uaz11 at yahoo.fr> a ?crit : > I can't understand the difference between the GFun node and the kernel_function. sspec can't be completely irrelevant, I presume. Well, for most practical purposes, sspec is irrelevant. It is only used in freshly type-checked AST, until Frama-C's internal tables are properly filled. It's not a stage where plug-ins intervene much (in fact, there isn't any hook to do so). > The only thing changing is indeed the vspec, but it changes with regards to what is in the function itself, we need to process the body (with vglob_aux) in order to get "what to put" in the postcondition (with vspec). OK, then you're right, it makes sense to use vglob_aux to do that. > > So we need to also override vglob_aux. > The thing is, we don't know the specific order in which these two (vglob_aux and vspec) are gonna be called. the spec is somehow a child of the function, thus vspec is called after vglob_aux (on the other hand, an action in ChangeDoChildrenPost for vspec will be performed before an action in ChangeDoChildrenPost for vglob_aux) > Isn't there an easier way to use Visitor.current_kf and set_current_kf, to link the generated GFun node, with the associated kernel_function? Unfortunately no: current_kf always refer to original function being visited. In fact, since the visitor can return more than one global (or for that matter, to turn a decl into def or vice-versa), it is not really possible to have a current_kf for the new function in the general case. Only the original one is meaningful. -- Virgile Prevosto Ing?nieur-Chercheur, CEA, LIST Laboratoire de S?ret? des Logiciels +33/0 1 69 08 82 98