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