--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on May 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Loops & variable reference.



Hello,

Still on the frama-c plugin for CerCo, we need to treat loops.
We've done some tests, and something odd happens everytime we try to process a loop : the visitor goes through it twice.
We tried the minimum : 

match s.skind with 
| Loop _ -> Format.printf "\n \n\n=> LOOP \n"

When we test with a file with no loops, it doesn't print anything, but if we have only one loop, it prints two "LOOP"
with 4, it prints 8 "LOOP"...

Does it go through the loops twice?
--
On the same subject, we need to test if the loop is secure : meaning the variable controlling it is not referenced anywhere else.
Is there a quick way to test if a reference to a variable has been stored elsewhere?

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/20110509/eeed4f56/attachment.htm>