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] Unroll_Loop

Hello,

Le mar. 03 mai 2011 20:31:59 CEST,
zakaria chihani <uaz11 at yahoo.fr> a ?crit :

> for (i= 0 ; i< 10; i=i+1) ;
> In order to assure that this loop will be executed 10 times, we have to check if
> ?- The i variable is not changed in the body.
> ?- That its address isn't referenced anywhere.
> ?- The bounds are known (0 - 10) 
> ?- The incrementation is fixed.
> 
> We noticed that For loops change into while loops.
> i=0;
> while i<10{
> ...
> i=i+1;
> } 
> 

Yes, there's only one kind of loop in Cil's AST. However, there is
another AST, the one generated by the parser. You might want to take
advantage of Frontc.add_syntactic_transformation, that allows to
perform transformations to this AST before is type-checked and
normalized, and of Cabsvisit module (also in cil/frontc). Beware that
this AST does not have all the properties of Cil (for instance,
variables are identified by strings, without link between declaration
and use).

Best regards, 
-- 
E tutto per oggi, a la prossima volta.
Virgile