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
- Prev by Date: [Frama-c-discuss] trouble debugging assertions
- Next by Date: [Frama-c-discuss] trouble debugging assertions
- Previous by thread: [Frama-c-discuss] trouble debugging assertions
- Next by thread: [Frama-c-discuss] arbitrary buffers in analysis
- Index(es):