--- layout: fc_discuss_archives title: Message 30 from Frama-C-discuss on August 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] my first frama verification



I just got done my first frama verification (thanks for the
help so far!).  It is here:

http://www.thenewsh.com/~newsham/frama/knock-3.tgz

I ended up going the brute force method of cranking up the
slevel VERY high and letting frama analysis run for hours.
I am unsure how to properly tune the analysis to make it more
efficient.  Right now my analysis run was 13hrs.  I would have
preferred to perform more comprehensive analysis but I kept
my buffer sizes reasonable to keep the analysis time reasonable.

If anyone has any pointers to where I could have used hints
such as function-specific slevels to keep the analysis time
down, I would love to hear some advice.  I've tried reorganizing
some of the setup in different ways but the one I ended up using
seemed to be the only one that worked....

Also, I put down some notes about what the analysis means
in the proof.txt file.  If anyone notices anything important I
should have mentioned that I forgot, please let me know.

I would also like to try other mechanisms for analyzing this
code.  Would it be feasible to use Jessie to analyze the components
in a more modular manner?  Are there some strategies for
using the value analysis in a more modular way that you would
recommend (for example, if I could somehow prove that hmac
was safe, in isolation, and then ommit the hmac implementation
from the whole program analysis).  What about other plugins
to frama-c and why3?

-- 
Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150820/af0dc846/attachment.html>