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] [Jessie] Assert clause not proved

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>