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 18:01, Tim Newsham a écrit :
> all of the warnings go away in frama-c if I use the parameters
> in my ./Frama file (in the tgz).  It seems if I crank up the
> slevel high enough, and use the val-split-return-auto
> argument, it tries enough paths to know the relation between
> the buffer and the sz in each analysis path. very brute force...

I'm surprised that you have no warning using a value range for "sz" 
instead of a constant value, but if you say so.

Next time, save the analysis log in a file.

> What dead code are you seeing?  Everything in seq.c should
> be important and useful.

It appears that -lib-entry option triggers a different behaviour in 
open-source Frama-C and TIS Analyzer for fopen() result. Without this 
option, I found no warning on your code (sz == 256, verification took 
1min) and the dead code disappeared (I did not make an exhaustive review 
though).


DISCLAIMER²: I just wanted to compare very quickly the behaviour of TIS 
Analyzer on your code, so I haven't made a detailed review of the option 
used, the driver and analysis result. I might have missed points that 
invalidate my analysis result.


There is still one of your assertion which is not proved (in 
frama-driver.c, just after the call to auth()). Interestingly, the 
postcondition of auth(), which is equivalent to this assert, is proved. 
I suspect WP (or Jessie) could be used to make the logical consequence 
in frama-driver.c and prove the assert but I did not try it. Or only use 
Value analysis and just proper re-writing of the logical expressions (I 
did some attempts, without much success).

Nonetheless, TIS Analyzer produces results in short time (1min vs. 
818min), which is encouraging. It would be interesting to see if one 
could gain some time using only the open-source version but I 
unfortunately don't have time for this (and already spent too much time 
in this use case ;-) ).

I had a quick look at your proof.txt file and found no obvious missing. 
You'll probably need to detail *all* analysis parameters, as each one of 
them could influence the analysis (e.g. -lib-entry). But your Frama 
script gives the definitive answer, so probably better just to reference it.

Best regards,
david