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