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