--- layout: fc_discuss_archives title: Message 43 from Frama-C-discuss on October 2013 ---
Dear Claude, Thank you for your reply. We are sending you an excerpt of the code. In this example, there are a series of null values, because it is a particular instance of our case study. We are verifying part of an embedded aerospace control software that has about 12,000 SLOC distributed in several functions. The code has divisions and sqrt function. We need to assure that the sqrt argument is a positive value and the denominator is not null. However there is a sequence of calculations and assignments in order to obtain this argument and denominator. Our reasoning is to assure values to the variables in the intermediate calculations in order to prove the final calculation. Is our reasoning correct? We are sending a screenshot of the Frama-c analysis. As was suggested we included the ghost variables and assert clauses to prove the chain of the calculations. However, we noticed that after including them, some clauses were not proved due to time out, even with time limit set to 300s. Regards, Nanci, Rovedy and Luciana ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Treat the Earth well. It was not given to you by your parents, it was loaned to you by your children. (Kenyan proverb) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ On Thu, Oct 10, 2013 at 9:33 AM, Claude March? <Claude.Marche at inria.fr>wrote: > > > 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 | > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131011/bd735563/attachment-0001.html> -------------- next part -------------- A non-text attachment was scrubbed... Name: screenshot1.png Type: image/png Size: 198107 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131011/bd735563/attachment-0001.png> -------------- next part -------------- A non-text attachment was scrubbed... Name: siteZero2.c Type: text/x-csrc Size: 4263 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131011/bd735563/attachment-0001.c>