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: Claude.Marche at inria.fr (Claude Marché)
  • Date: Tue, 01 Oct 2013 15:39:28 +0200
  • In-reply-to: <CAEtoXR1woE5aOS64G+rrr6t2qsFX=Dy+aV-3j-MsYOfMR0YTpw@mail.gmail.com>
  • References: <CAEtoXR1woE5aOS64G+rrr6t2qsFX=Dy+aV-3j-MsYOfMR0YTpw@mail.gmail.com>
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                    |