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



Hi,

it's interesting that you mention you can prove it with z3. In my
experience with the WP plugin, I cant prove anything with Z3 (4.3.2) save
one or other random PO.

I usually rely on CVC3 (2.4.1)


2013/5/6 Lo?c Correnson <loic.correnson at cea.fr>

> 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
>
>
>
> _______________________________________________
> 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
>



-- 
Cumprimentos,
Cristiano Sousa
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130507/d581cd37/attachment.html>