--- layout: fc_discuss_archives title: Message 7 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!

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/20110503/6b6dde91/attachment.htm>