--- layout: fc_discuss_archives title: Message 52 from Frama-C-discuss on April 2011 ---
Hello! The current_kf function works perfectly, thank you very much! Now, in a whole other part, we need to infer properties on bound for loops, mainly to annotate based on the number of iterations. e.g : 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; } We only treat "well formed for loops", so we can either call the CFG, so that each time we get a Loop statement, we check the prec field to verify that it's the initialisation of the variable inside the condition, or we keep, in an additional variable, the previous stmt. Now the question is this : is there some features in Frama-c that can help us do things more properly? Generate invariants for "well formed for loops?" ? Thank you for your help! H. Zakaria Chihani. -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110429/c533b2ee/attachment.htm>