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] Loops & variable reference.

  • Subject: [Frama-c-discuss] Loops & variable reference.
  • From: uaz11 at yahoo.fr (zakaria chihani)
  • Date: Mon, 9 May 2011 08:17:06 +0100 (BST)
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>