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

  • Subject: [Frama-c-discuss] [Jessie] Assert clause not proved
  • From: Claude.Marche at inria.fr (Claude Marché)
  • Date: Thu, 10 Oct 2013 14:33:52 +0200
  • In-reply-to: <CAP6nMJRa3XKrW=7GTZX1FCUeGpQpKz1HAbbvX7Ak1B_MWyWniQ@mail.gmail.com>
  • References: <CAEtoXR0kvDu5+NMAqEmCQkpQJRuGcagAZnURjAth_m=wxyQK+g@mail.gmail.com> <52539AD3.6070801@inria.fr> <5253FBAC.6070700@inria.fr> <CAEtoXR0XQ-OKs5oDCu7L3uSn-S8zMCm3BtPYKNxtFYJACq-7cA@mail.gmail.com> <CAP6nMJRa3XKrW=7GTZX1FCUeGpQpKz1HAbbvX7Ak1B_MWyWniQ@mail.gmail.com>

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                    |