Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 151
    • Issues 151
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 9
    • Merge requests 9
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Merge requests
  • !554

Add persistent points-to predicate to Iris

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Simon Friis Vindum requested to merge simonfv/iris:persistent-points-to-2 into master Oct 26, 2020
  • Overview 118
  • Commits 11
  • Changes 14

This is the same as !493 (closed) but based on !486 (merged). The overall description in !493 (closed) still applies.

Notation

As in the previous MR I've used the notation l ↦□ v for the new persistent points-to predicate and changed the notation used by gen_inv_heap. In the original MR description I argued for this choice and @jung replied with some additional arguments to consider. I think the conclusion is that using l ↦□ v for the persistent points-to predicate is a good idea but that we need to come up with some other notation for gen_inv_heap than what currently is in this MR.

Edited Dec 18, 2020 by Ralf Jung
Assignee
Assign to
Reviewer
Request review from
Time tracking
Source branch: persistent-points-to-2