--- layout: fc_discuss_archives title: Message 149 from Frama-C-discuss on September 2013 ---
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 -------------- next part -------------- A non-text attachment was scrubbed... Name: gwhy.png Type: image/png Size: 30049 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130930/4c0fcc52/attachment-0001.png> -------------- next part -------------- A non-text attachment was scrubbed... Name: teste.c Type: text/x-csrc Size: 803 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130930/4c0fcc52/attachment-0001.c>