--- layout: fc_discuss_archives title: Message 74 from Frama-C-discuss on October 2013 ---
On 18/10/2013 09:26, David MENTRE wrote: > 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? If you are using the plugin Jessie or the plugin WP, you can already prove your goal using why3. And why3 has a session mechanism through the commands why3ide, why3replayer and why3session. A session allow you the kind of cache David is referring. In fact GNATprove also use why3 for that ;). Best regards, -- Fran?ois