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] Debugging huge theories

Hello Yegor,

I wanted to run your example through Frama-C but the file hsearch.h  
is  missing.
I also noticed that some of loops do not have loop annotations, in  
particular  the do-while
loop.

Regards Jens

Am 22.12.2009 um 02:50 schrieb Yegor Derevenets:

> Hello, All!
>
> There is an implementation of hsearch function described here:
> http://www.opengroup.org/onlinepubs/000095399/functions/hsearch.html
>
> This implementation to be verified (with some ACSL code) is present  
> here:
> http://www.vsi.ru/~yegor/tmp/hsearch.c
>
> In order to decrease the size of theory the hsearch function was split
> into two functions: compute_hash and hsearch (the rest).
>
> As you see, hsearch function has many behaviour cases with
> complicated conditions in assumes and ensures clauses.
>
> Originally verification was to be done completely in PVS, but it
> seems to be whole life-consuming task to prove 21mb of lemmas
> in PVS. Partially, because he almost dies for several hours garbage
> collecting trying to parse files with hundreds of lemmas.
>
> It looks like the only choice left is automatic provers.
> Simplify proves about 87% of lemmas.
> Alt-Ergo proves several of those not proved by Simplify.
>
> Any ideas on proving what has left?
> Here it's not the case, when one (or at least I) can have a look
> at failed statement and understand why it's wrong.
>
> My specification definitely misses variant and invariant for
> do-while loop in hsearch(), but since Simplify generates
> counter-examples, there are also false statements,
> gWhy can show me them in beautiful GUI, but what's next?
>
> Are there any approaches to debugging big not-very-obvious
> theories like this?
>
> -- 
> Yegor Derevenets
>
> _______________________________________________
> 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/20091222/26629510/attachment.htm