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] my first frama verification

  • Subject: [Frama-c-discuss] my first frama verification
  • From: tim.newsham at gmail.com (Tim Newsham)
  • Date: Thu, 20 Aug 2015 12:13:56 -1000
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>