--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on October 2013 ---
Le 09/10/2013 19:35, Nanci Naomi a ?crit : > Thank you for your replies. We used the ghost variables and the VCs were > proved in our reduced code version. > > However, there are several similar assignments in our legacy code and we > included the ghost variables and the assert clauses to all of them. > After that, the frama-c analysis seems to run slowly, Gappa does not > prove some assert clauses (External prover call failed) and Alt-Ergo > proves them, but it was necessary to enlarge the time limit to avoid > time out. We set the time limit to 300s and there are some not proved > assert clauses yet. > > According to Claude, the ghost variables is a heavy solution. Is not > possible to use ghost variables several times? For sure you can use as many ghost variables as you like. > Are there other solution? I have no other suggestion, sorry > We are only verifying a legacy code and we do not intend to modify it. If you can send an excerpt of what should be proved but is not, I could try to help - Claude -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | Universit? Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex |