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