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 125
    • Issues 125
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 15
    • Merge Requests 15
  • Operations
    • Operations
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
  • Why3
  • why3why3
  • Issues
  • #130

Closed
Open
Opened Jun 05, 2018 by Ghost User@ghost

Why3 doesn't extract sequence of statements, only the last one

Using today's master branch (commit e55e1d35), I'm running into the following issue.

If I have an .mlw file with a sequence of statements such as the following:

$ cat unitbug.mlw 
module UnitBug
  use import io.StdIO

  let test () =
    print_int 1;
    print_int 2;
    print_int 3

end

... and then I extract it with the following command:

$ why3 extract -D ocaml64 unitbug.mlw -o unitbug.ml

... this is the resulting, extracted file:

$ cat unitbug.ml
let test (us: unit) : unit =
  Pervasives.print_int (Z.to_int (Z.of_string "3"))

Not 100% sure this is a bug, but I expected the extracted file to contain 3 calls to Pervasives.print_int, one for each of the integers (1, 2, 3).

To upload designs, you'll need to enable LFS and have admin enable hashed storage. More information
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: why3/why3#130