Open wandernauta opened 1 month ago
Looks like the constantFinalFields
rewrite is not generics-aware. Post-rewrite f
should get a generics argument itself. Since generics support in VerCors is at the moment spotty at best, it would be fine to not support this use case for now, and throw a usererror here whenever a (static) final field occurs in a class. Making the constantFinalFields
class generics-aware should also not be too complicated a task.
The following PVL program causes the
constantFinalFields
rewrite to generate an AST that no longer typechecks, which triggers a VerCors crash:The
col
file before the rewrite is:The
col
file after the rewrite is:This issue was found by fuzzing.