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

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