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