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, 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