--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on April 2011 ---
Le jeu. 07 avril 2011 00:58:48 CEST, zakaria chihani <uaz11 at yahoo.fr> a ?crit : > 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