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

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