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: Mon, 30 Sep 2013 16:09:23 -0300
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>