GitLab

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.