--- layout: fc_discuss_archives title: Message 74 from Frama-C-discuss on October 2013 ---
[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