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] Jessie plugin - more than 6, 000 VCs generated
- Subject: [Frama-c-discuss] Jessie plugin - more than 6, 000 VCs generated
- From: dmentre at linux-france.org (David MENTRE)
- Date: Fri, 18 Oct 2013 09:26:01 +0200
- In-reply-to: <CAP6nMJRzieqorh4wwF+E6uaYCmrhuB9RJ-BmWD2Ny63x72rxew@mail.gmail.com>
- References: <CAP6nMJSdSknD8vZDppXi0aNz55zmyi_98ajThBmcMOn3Buks7Q@mail.gmail.com> <CAC3Lx=aQtcuE8VQXU-eBTS1Gcj3+F-9y_msTUFrArAZ7Ne2E2g@mail.gmail.com> <CAP6nMJRzieqorh4wwF+E6uaYCmrhuB9RJ-BmWD2Ny63x72rxew@mail.gmail.com>
Hello, 2013/10/17 Nanci Naomi <nnarai at gmail.com>: >> 3. Buy/rent a faster machine. > > > our machine is a Mac Boo Pro, processor: 2.9 GHz Intel Core i7, memory: 8 > GB. > this example with about 2,000 VCs is verified in about 10 minutes, but our > original source code with 6,000 VCs is analyzed very slowly, the Alt-ergo > prover takes about 24 hours without finishing the analysis. Probably the main issue is that each time you make a modification, you need to redo *all* the VCs. Not very usable in practice. GNATprove (technology similar to Frama-C but applied on Ada) provides a cache mechanism that avoids re-doing VCs that haven't changed. Maybe a future improvement for Frama-C? > then, we replaced the suggested annotation by this one: > /*@ assigns flag; > @ ensures (a && !a1) ==> flag == time1; > @ ensures !(a && !a1) ==> \old(flag); > @*/ > if(a == TRUE && a1 == FALSE) > { > flag = time1; > } > > it ran, but how do this work? > Sorry, but I did not understand how these annotations will make possible to > run the analysis in a shorter time. [Claude will probably correct me. ;-) ] This annotation substitutes, within the logical framework of Jessie, the "if" piece of code by the given assertion which is equal to one (or two?) logical formula (((a && !a1) ==> flag == time1) && ( !(a && !a1) ==> \old(flag))). Then, when the weakest precondition generation algorithm is applied, this unique logical formula is used instead of the 3 logical formulas generated from the "if" construct, thus the reduction on the number of VCs. You would obtain the same result by putting part of your code into another function, with a proper contract to represent the corresponding code and call it from the original function. Which brings me to a fourth proposal: 4. Cut the original code into several sub functions, with for each called function a contract summarizing the corresponding code. I know this approach is sometimes used into other formalisms, for example using LOCAL_OPERATIONS in B Method. Best regards, david
- Follow-Ups:
- [Frama-c-discuss] Jessie plugin - more than 6, 000 VCs generated
- From: francois.bobot at cea.fr (François Bobot)
- [Frama-c-discuss] Jessie plugin - more than 6, 000 VCs generated
- References:
- [Frama-c-discuss] Jessie plugin - more than 6,000 VCs generated
- From: nnarai at gmail.com (Nanci Naomi)
- [Frama-c-discuss] Jessie plugin - more than 6, 000 VCs generated
- From: dmentre at linux-france.org (David MENTRE)
- [Frama-c-discuss] Jessie plugin - more than 6, 000 VCs generated
- From: nnarai at gmail.com (Nanci Naomi)
- [Frama-c-discuss] Jessie plugin - more than 6,000 VCs generated
- Prev by Date: [Frama-c-discuss] [value analysis] calls the system library function abort or exit will result in NON TERMINATING FUNCTION. Why?
- Next by Date: [Frama-c-discuss] [value analysis] calls the system library function abort or exit will result in NON TERMINATING FUNCTION. Why?
- Previous by thread: [Frama-c-discuss] Jessie plugin - more than 6, 000 VCs generated
- Next by thread: [Frama-c-discuss] Jessie plugin - more than 6, 000 VCs generated
- Index(es):