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

Once again hi :)

I'm having more and more problems with the WP plugin in this new version of
frama-c

After applying the previous patches suddenly i cant use the 'unsafe casts'
option in one of my functions

I get the following error:

Current source was: ungetc.c:40
The full backtrace is:
Raised at file "hashtbl.ml", line 353, characters 18-27
Called from file "hashtbl.ml", line 361, characters 22-38

Unexpected error (Not_found).

code to reproduce the error: http://pastebin.com/AjDHf2jJ

Thanks


2013/5/7 Cristiano Sousa <cristiano.sousa126 at gmail.com>

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



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