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

[Frama-c-discuss] New version of Jessie



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>