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