Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Register
  • Sign in
  • RefinedC RefinedC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 22
    • Issues 22
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 5
    • Merge requests 5
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Environments
    • Releases
  • Monitor
    • Monitor
    • Metrics
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • RefinedCRefinedC
  • Issues
  • #31
Closed
Open
Issue created Dec 09, 2020 by Rodolphe Lepigre@lepigreMaintainer

What generation condition for types?

Currently a new RefinedC type is automatically generated on a struct if either:

  • it has a refinement (i.e., at least one rc::refined_by annotation),
  • it has a rc::ptr_type annotation (in which case there can be no rc::refined_by, and the refinement is unit).

One might wonder, can we relax this? And would this be useful in practice?

I have tried relaxing this behaviour but there is no obvious way to do this. The problem is that we explicitly rely on the fact that no types are generated in two cases:

  • nested structs, as for mpool_locked_inner in https://gitlab.mpi-sws.org/iris/refinedc/-/blob/master/examples/mpool.c#L75,
  • and union cases (which are also nested structs), as empty in https://gitlab.mpi-sws.org/iris/refinedc/-/blob/master/examples/mutable_map.c#L22.

One solution is to add a rc::only_nested annotation that instructs the front end not to generate a type. However that is a bit annoying in the case of unions. However there is no easy way to avoid this since the front end does not distinguish structs that are nested from those that appear at the top level.

Another possible solution (not tried yet) is to move the rc::union_tag annotation into structs (and not have it as field annotation). This annotation would also disable the generation of a type, while keeping the information we need for the struct.

Assignee
Assign to
Time tracking