--- layout: fc_discuss_archives title: Message 30 from Frama-C-discuss on August 2015 ---
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>