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