--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on October 2013 ---
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 |