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>
- Follow-Ups:
- [Frama-c-discuss] my first frama verification
- From: anne.pacalet at free.fr (Anne Pacalet)
- [Frama-c-discuss] my first frama verification
- From: dmentre at linux-france.org (David MENTRE)
- [Frama-c-discuss] my first frama verification
- Prev by Date: [Frama-c-discuss] arbitrary buffers in analysis
- Next by Date: [Frama-c-discuss] headers question
- Previous by thread: [Frama-c-discuss] arbitrary buffers in analysis
- Next by thread: [Frama-c-discuss] my first frama verification
- Index(es):