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 version of Jessie

  • Subject: [Frama-c-discuss] New version of Jessie
  • From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
  • Date: Tue, 8 Oct 2013 16:08:16 -0300
  • In-reply-to: <524AD090.4030706@inria.fr>
  • References: <CAEtoXR1woE5aOS64G+rrr6t2qsFX=Dy+aV-3j-MsYOfMR0YTpw@mail.gmail.com> <524AD090.4030706@inria.fr>
Hi,

We did not understand what is the bug.

We have other examples with local variables in the loop assigns clause
and they run and the VCs are proved.

In fact, without the loop assigns clause the example runs, but keeping
this clause and without the the modf2 function the code runs too
(attached source code).

According to these tests, the bug seems not to be the loop assigns
clause. What would be the problem?

We are using the Why3 Verification Platform 0.81, Fluorine-20130601.

Best regards,
Nanci, Rovedy and Luciana

2013/10/1, Claude March? <Claude.Marche at inria.fr>:
>
> Hi,
>
> It is not a well-known bug, but at least I am aware of it. When using
> the Jessie plugin, you should not add local variables in the "loop
> assigns" clause.
>
> So, in your example, remove the loop assigns and it will work.
>
> Sorry for the inconvenience.
>
> - Claude
>
>
>
> Le 30/09/2013 21:09, Rovedy Aparecida Busquim e Silva a ?crit :
>> Hi,
>>
>> We have a problem running the attached source code in the Why3
>> Verification Platform 0.81, Fluorine-20130601 and the more updated
>> provers installe in the last week.
>>
>> The GWhy window opened, but it did not work and showed an error message
>> window:
>> "Error while reading file '../test.mlw': File "test/../test.mlw", line
>> 384, characters 72-90: This term has type int but is expected to have
>> type ref int"
>>
>> the same source code run in the Carbon version and all 7 VCs were proved.
>>
>> Why the error in the new version?
>>
>> We run some tests and we noticed that without the loop assigns clause
>> the new version, works but it does not prove all VCs.
>>
>> Best regards,
>> Nanci, Rovedy e 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
>>
>
> --
> Claude March?                          | tel: +33 1 72 92 59 69
> INRIA Saclay - ?le-de-France           |
> Universit? Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
> F-91405 ORSAY Cedex                    |
>
>
> _______________________________________________
> 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 --------------
A non-text attachment was scrubbed...
Name: teste1.c
Type: text/x-csrc
Size: 795 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131008/2cc988b7/attachment.c>