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] [Why3-club] why3 / why2 and jessie -- a few questions

  • Subject: [Frama-c-discuss] [Why3-club] why3 / why2 and jessie -- a few questions
  • From: dmentre at linux-france.org (David MENTRÉ)
  • Date: Tue, 18 Aug 2015 21:03:42 +0200
  • In-reply-to: <CAGSRWbiW_Hc38Y6Zne6s=LVHffLv8_iRnREk49Uhk1PdnRTemQ@mail.gmail.com>
  • References: <CAGSRWbiW_Hc38Y6Zne6s=LVHffLv8_iRnREk49Uhk1PdnRTemQ@mail.gmail.com>
Hello Tim,

Le 2015-08-04 22:31, Tim Newsham a écrit :
> Finally, I wanted to know realistically how large of a C program I can
> expect to analyze. Can why, frama-c and plugins deal with realistic programs
> that are on the order of size and complexity of something like openssl?

Complexity of openssl, yes. TrustInSoft has verified absence of Run Time 
Error in PolarSSL, another SSL library: 
http://trust-in-soft.com/polarssl-verification-kit/ (TrustInSoft 
Analyzer is essentially Frama-C / Value analysis + some proprietary 
plug-ins to accelerate and scale the analysis).

Size : I've been told that Frama-C can verify programs up to 150,000 
lines of code (150 kloc), maybe more. PolarSSL is about 6 kloc. EDF 
programs are about 50 kloc each. Airbus and Dassault Avation are also 
applying Frama-C and WP. For Dassault Aviation, the reported program 
size is about 50 kloc (dataflow verification + proof on variable domain 
bounds).

I routinely verify 30-50 kloc with TrustInSoft Analyzer.

Now, as Virgile said, this strongly depend on the kind of properties you 
want to verify. For big programs (50 - 150 kloc), this is "simply" 
absence of Run Time Error with Value analysis (which are already complex 
properties to prove on real programs). WP and Jessie are applied on 
smaller programs.

Astrée (one of Frama-C / Value analysis competitor) is reported to 
verify 300 kloc (Airbus flight control software).

I don't know of any sound tool (Astrée, Frama-C and Polyspace) able to 
cope with 1 - 10 millions lines of code as found in programs like Linux 
kernel, LibreOffice or Firefox. Facebook's Infer 
(http://gulliver.eu.org/program_dev_check_environments#infer) is 
targeting such big code base but as far as I understood it is unsound.

> When dealing with a complete program is it typically analyzed in
> its entirety or is it more typical to perform analysis in smaller units
> such as a file size?

As Virgile said, with WP and Jessie you can have a modular, per function 
approach (by verifying the call tree upward).

With Value analysis, you would rather verify the whole program in one 
chunk, maybe in several big chunks if some parts are very complex.

> Would this require manually crafting a command
> line to effectively ``build'' the whole thing inside frama-c/why?

Yes, most of the time you need to adapt your source code to "fit within" 
Frama-C (either with WP/Jessie or Value analysis) : command line plus 
some code modification. Ideally one would develop the source code 
simultaneously with formal verification. In practice this is far from 
being the case and some tweaks are needed (like syntactic loop unrolling).

Best regards,
david