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] question about a simple example and jessie

> - one of the invariants is false, and your CVC3 is correctly using it
> to prove both the post-condition and its negation.
>    

This is highly probable, as I get 'timeouts' and 'unknown' for some 
invariants. Maybe the prover cannot prove the invariant is wrong, but 
cannot prove it right either.

> Could you clarify what the diagnostic of each of alt-ergo and CVC3 is
>    
Where can I find this? Is this in the jessie log file? If I run CVC3 and 
Alt Ergo back to back, does it include both results in the log file?

thanks,
naghmeh