--- layout: fc_discuss_archives title: Message 12 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



Hello,

I can't understand the difference between the GFun node and the kernel_function. sspec can't be completely irrelevant, I presume.


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). 


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. 
We could, in the new vglob_aux, generate a map to keep pairs of the form (function_name, thing_to_put_in_vspec) but are we sure that vglob_aux on some function f is always going to be called before the vspec on the spec of the same function f?

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?


Thank you.

PS : Here's to keep track :)



> Hello! Me again!
> 
> Right, so everything works, thank you so much for your help!
> But when we use 
> ? Cil.d_global Format.std_formatter annotatedFun ;
> It prints, on the std_out, exactly what we want, the ensure clause is right where we need it.
> 
> But there's nothing in the outed file, it doesn't change the GFun nodes into Annotated GFun nodes (adding an ensure clause).
> The colored parts are of interest...
> ___________________________________________
> ? method vglob_aux g=
> ??? begin match g with
> ????? | GFun (oldFundec,location1) ->
> ????? (*...other things here...*)
> ??? ? let newFundec = ??? ?? 
> ??? ??? {oldFundec with sspec = newSpecc} in
> ??? ? let annotatedFun = GFun (newFundec,location1)
> ??? ? in 
> ??? ?? Cil.d_global Format.std_formatter annotatedFun ; (*shows an annotated fun*)
> ???? (*? ChangeDoChildrenPost ( [annotatedFun], fun x -> x)? didn't work either*)
> ??? ?? ChangeToPost( [annotatedFun], fun x -> x)???? (*Doesn't seem to be working...*)
> ????? | _ ->? JustCopy
> ??? end
> ?____________________________________________ ??? 
> 
> In case ChangeToPost wasn't the problem, here's how we do the copy afterwards,
> In another .ml, we apply CerCo, it passes to cost, here, a Cabs.file, the name of the incrementation function, and the global var to be incremented.
> 

in Frama-C, the sspec field is not relevant: it's the spec field in the
associated kernel_function that reflects the real annotation (the dev's
manual for more information). If the only thing that you're changing in
GFun is the specification, I guess that DoChildren on GFun and
overriding vspec is the easiest way to obtain what you want: the
generic visitor itself will take care of putting the new spec in the
appropriate place.

Note however that vspec is visited from 3 places
- function prototypes (without a corresponding def)
- function definitions
- statement contract

You can discriminate between the three with self#current_func (None for
prototype) and self#current_statement (None for function definition
(and prototype of course)).

All definitions and prototypes have a specification, that can be empty,
so vspec will be called for each definition (it is called from a
GVarDecl iff there's no corresponding GFun to avoid visiting the same
spec twice).

Hope this helps,
-- 
E tutto per oggi, a la prossima volta.
Virgile


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110411/0d347133/attachment.htm>