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] Problem with ChangeDoChildrenPost

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