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 18
    • Merge Requests 18
  • 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
  • #184

Closed
Open
Opened Sep 17, 2018 by Guillaume Melquiond@melquionOwner

Improve the "diverges" effect

This is a followup on !19 (merged) . After a long brainstorming session with @paskevyc , here is the system we have devised to improve the diverges effect, so that it covers a lot more cases.

Regarding the implementation, divergence is currently encoded by a boolean named Ity.eff_oneway. We propose to replace this boolean by a tristate value that says ghostifiable (1) or non-ghostifiable terminating (2) or possibly non-terminating (3). State 2 is the new one; the semantics of the other two is left unchanged. The ordering is from left to right, i.e., combining a state-i expression with a state-j expression gives an expression with state max i j. Moreover, a val declaration with a given state can only be refined with a let definition with a state lower or equal. A val diverges declaration has state 3, and so has a non-terminating let expression. A ghost expression can only have state 1. A let definition with state 3 must be explicitly specified as diverges. So, the two critical points are that a let definition with state 2 does not need to be specified as such, and that it can be declared neither ghost nor function.

Regarding the surface language, we just need a new effect keyword to specify that a val declaration has state 2. For now, we do not give any way for the user to split state 2 into several subcategories for the sake of documentation; this can come later.

Applications of this new state are:

  • peano.Int63.to_in63 @bobot ;
  • alloca and c_assert @rrieuhel ;
  • read, write, random, etc.

Note that, in the later applications, e.g. random, we no longer need a dummy writes specification (if we are not interested in a bit-precise modeling). Note also that state 2 has been described as terminating, but it should be understood as terminating if the environment is cooperating. For example, a WhyML program with state 2 can end up being killed by SIGPIPE during a write call.

I am assigning this report to @rrieuhel . But @bobot, if you need it soon, do not hesitate to take over.

Edited Sep 17, 2018 by Guillaume Melquiond
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#184