--- layout: fc_discuss_archives title: Message 131 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, Jens.

2009/12/22 Jens Gerlach <jens.gerlach at first.fraunhofer.de>:
> I wanted to run your example through Frama-C but the file hsearch.h is
> missing.
Sorry, my fault.
http://www.vsi.ru/~yegor/tmp/hsearch.h

> I also noticed that some of loops do not have loop annotations, in
> particular ?the do-while loop.
Exactly, do-while was the last loop left without annotations.
I've done some thinking and added both variant and invariant to the loop.
Updated file http://www.vsi.ru/~yegor/tmp/hsearch.c

You can skip annotations of isprime, hcreate and hdestroy, since
verifying them is not my primary goal. (And these functions are
commented out.)

Obviously, some annotation are wrong (the function is not trivial,
and I'm a human). The quesiton is how to detect which and why,
and fix them in a reasonable amount of time. Maybe some ideas
about what to begin with?

-- 
Yegor Derevenets