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 120
    • Issues 120
    • 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

Mise à jour terminée. Pour connaître les apports de la version 13.10.3 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/03/22/gitlab-13-10-released/
https://about.gitlab.com/releases/2021/03/31/security-release-gitlab-13-10-1-released/
https://about.gitlab.com/releases/2021/04/01/gitlab-13-10-2-released/
https://about.gitlab.com/releases/2021/04/14/security-release-gitlab-13-10-3-released/

  • Why3
  • why3why3
  • Issues
  • #315

Closed
Open
Created May 07, 2019 by Benedikt Becker@bbeckerDeveloper

Too much ghostification?

In the following example, the ghostification that is introduced by line 16, is expanded to line 12, which results in a compilation error.

The example code works fine when f is non-recursive, when the ghost keyword is removed from line 16, or when an ; () is added after line 16.

$ cat test.mlw
module Test
  use option.Option

  let ref x = ()

  exception E
  type t = A | B

  let rec f (t: t) diverges raises { E -> true } =
    match t with
    | A ->
      x <- () (* Line 12 *)
    | B ->
      try
        f t;
        ghost () (* Line 16 *)
      with E ->
        raise E
      end
    end
end
$ why3 extract --modular -D ocaml64 -L . test.Test -o /tmp
File "./test.mlw", line 12, characters 6-13:
This expression makes a ghost modification in the non-ghost variable x
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
1.5.0
Milestone
1.5.0
Assign milestone
Time tracking
None
Due date
None