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