--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on October 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Jessie] Assert clause not proved




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                    |