[Why3-club] Strange type error message on a ref array

Johannes Kanig kanig at adacore.com
Wed Nov 28 15:52:55 CET 2012

On 11/28/2012 03:25 PM, David MENTRE wrote:
> However, when I apply this pattern to a data structure with an array,
> it fails with a type error message I don't understand:

I also don't understand the error message. I understand why your program
is incorrect, but Why3 seems to point to the wrong place.

> """
> module Test2
>   use import ref.Ref
>   use import array.Array
>   type t = array int
>   val c : ref t

In Why3, you are not allowed to store mutable objects in other mutable
objects. Here, you are storing a mutable array in a reference. That is
not allowed in Why3 and I would expect Why3 to give an error message at
the declaration of c. The message you see is probably a consequence of
not rejecting this declaration ...

Johannes Kanig <kanig at adacore.com>

More information about the Why3-club mailing list