--- layout: fc_discuss_archives title: Message 130 from Frama-C-discuss on December 2009 ---
[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