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