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] New Frama-C version: Fluorine

Thanks for the report.

It's seems to be related to a problem in alt-ergo with the record theory : the addition of the helper assertions trigger more fact on record comparisons.
Without these helpers, alt-ergo give up very quickly (less than 1s), which can be a sign of incompleteness.
Goals are proven with Z3, though.

Regarding cvc3, it is indeed a why3 issue, if any.
	L.


Le 4 mai 2013 ? 19:07, Cristiano Sousa a ?crit :

> Hi,
> 
> I'm having a odd problem with proving a simple contract with the WP plugin. I'm forced to insert the assertions HELPER and HELPER2 in order to discharge all POs, when in the Oxygen release I didn't need this kind of assertions. Without HELPER, BOUND cannot be proved and without HELPER2 the post condition cannot be proved. Note: the rest of the assertions were inserted to help me pinpoint the problem.
> 
> http://pastebin.com/p5AdPN2n
> 
> Also, in the previous release of frama-c there was a problem with cvc3 processes not being killed. This problem now happens more ofter but i'm guessing this is a problem related to why and not frama-c.
> 
> Thanks!
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130506/69e89ba1/attachment.html>