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

[Frama-c-discuss] Difference between Kernel_function and GFun node



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