--- layout: fc_discuss_archives title: Message 85 from Frama-C-discuss on October 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Array problem - Jessie plugin



Thank you for your reply.

However, we need to prove without the pragma JessieFloatModel(math).

What is the problem?

Best regards, Luciana


2013/10/22 Eugene Kornykhin <kornevgen at gmail.com>

> Hi! You can use pragma to ask Jessie interpret floats as unbounded reals
> # pragma JessieFloatModel(math)
>
> After that Alt-Ergo discharges all VCs succesfully.
>
>
> Eugene
>
>
> On 21 October 2013 16:03, Luciana Burgareli <luciana.burgareli at gmail.com>wrote:
>
>> Hi,
>>
>> This is a very simple example, but it was not proved.
>>
>> If we slightly modify the code and we add an assignment to the Ang2[1]
>> (and the related assigns and ensures clauses), both the ensures clauses are
>> proved.
>>
>> Why is not the attached example proved?
>>
>> How to solve this problem?
>>
>> We are using the Jessie Plugin, Why3 Verification Platform 0.81,
>> Fluorine-20130601 and the provers Alt-Ergo 0.95.2, CVC3 2.4.1, Gappa 1.0.0
>> and Z3 4.3.2.
>>
>>
>> Luciana
>>
>>
>> _______________________________________________
>> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131024/a9b2478a/attachment.html>