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

  • Subject: [Frama-c-discuss] Unroll_Loop
  • From: uaz11 at yahoo.fr (zakaria chihani)
  • Date: Tue, 3 May 2011 20:31:59 +0100 (BST)
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>