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: dmentre at linux-france.org (David MENTRE)
- Date: Fri, 21 Aug 2015 09:00:53 +0200
- In-reply-to: <CAGSRWbgk8sbO4DKZ-ij8jbDALBgt8e7K4dAto-puDQZqbu+76Q@mail.gmail.com>
- References: <CAGSRWbgk8sbO4DKZ-ij8jbDALBgt8e7K4dAto-puDQZqbu+76Q@mail.gmail.com>
Hello Tim, Le 21/08/2015 00:13, Tim Newsham a écrit : > 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. Here is the strategy I am using: 1. Analyse the whole code with default slevel (=> lots of warnings) 2. Look at warnings *in the same order as found by Value analysis*. For the first one of them, look at the code: * If it is a loop, increase -slevel-function for this function up to the upper bound of the loop; * If there is no loop, look at values determined by Value analysis and triggering the warning. Try to find from where those values are coming from and why they have such wide domain, usually from previously called functions and the corresponding call tree. Look in those functions and try to increase the slevel using -slevel-function. 3. Go to 2 and repeat until you have no more warnings (or bugs to fix). In the end, I have a bunch of -slevel-function, but all other functions are using the default slevel. YMMV. I haven't look at your code, but it might appear that your specific code indeed needs hours to check due to some very complex functions. Or you need optimizations provided by TrustInSoft Analyser (for memcpy and the like functions). ;-) Another trick: use the -save and -load options to separate analysis and use of the GUI. Do the analysis using frama-c and -save. Then make a very basic script that simply calls "frama-c-gui -load previously-saved-analysis.save". That way, you can launch the GUI several times and very quickly, without having to wait hours for the analysis to finish. Best regards, david
- Follow-Ups:
- [Frama-c-discuss] my first frama verification
- From: dmentre at linux-france.org (David MENTRE)
- [Frama-c-discuss] my first frama verification
- References:
- [Frama-c-discuss] my first frama verification
- From: tim.newsham at gmail.com (Tim Newsham)
- [Frama-c-discuss] my first frama verification
- Prev by Date: [Frama-c-discuss] my first frama verification
- Next by Date: [Frama-c-discuss] arbitrary buffers in analysis
- Previous by thread: [Frama-c-discuss] my first frama verification
- Next by thread: [Frama-c-discuss] my first frama verification
- Index(es):