Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
why3
why3
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 122
    • Issues 122
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 20
    • Merge Requests 20
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • Why3
  • why3why3
  • Issues
  • #468

Closed
Open
Created Mar 25, 2020 by Mário Pereira@mariojppereiraDeveloper

Clone problem when type has nested regions

Consider the following example:

module A

  use seq.Seq, int.Int

  type t = private { ghost mutable view: seq int }

  val set (a: t) : unit
    writes { a.view }

end

module B

  use array.Array, int.Int, seq.Seq

  type t = {
    mutable data: A.array int;
    ghost mutable view: seq int;
  }

  let set (a: t) : unit
  = a.data[0] <- 42; a.view <- empty

end

module C

  use B

  clone A with type t, val set

end

I get an

Illegal instantiation for program function set:
unreferenced write effects in variables: a

error message because of the clone in module C.

I believe this is due to the fact that I am changing the elements of data, hence touching the region of the array. In fact, if I change data directly

let set (a: t) : unit
  = a.data <- make 0 42; a.view <- empty

Why3 is happy.

Apparently, the problem is being detected at line 1179 of pmodule.ml.

Given the recent updates on Why3 clone mechanism, am I missing something here? Is there a proper way to specify the effect of set in module A in order to to pass this clone, even when touching an inner region?

Note: this is a simplified example taken from the VOCaL library (cf, https://github.com/vocal-project/vocal/blob/master/vocal/proofs/why3/Vector_impl.mlw). Before merge request !347 (merged) we were able to clone function set as is.

Edited Mar 25, 2020 by Mário Pereira
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None