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 121
    • Issues 121
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 17
    • Merge Requests 17
  • 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

Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

  • Why3
  • why3why3
  • Issues
  • #160

Closed
Open
Opened Jul 11, 2018 by DAILLER Sylvain@sdaillerDeveloper

Counterexample for one-region record

In new_ide, when a counterexample is given for a type with only one mutable region, the id which is used to refer to a variable of such type is then reused for a variable of its only mutable type. The problem is that the model_trace is not changed. An example of this is (bench/ce/arrays.mlw):

module A

  use import int.Int
  use import array.Array

  let f2 (a:array int) : unit
    requires { a.length >= 2 }
    ensures { a[0] <> a[1] }
  = a[0] <- 42

end

It can be seen because the counterexample is a = (0 => 42...) instead of a.elts = (0 => 42 ....).

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
Reference: why3/why3#160