Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Recursively self-referential generic Java class causes MonomorphizeClass to not terminate #1279

Open
wandernauta opened this issue Nov 13, 2024 · 1 comment
Labels
A-Bug F-Java Frontend: Java F-PVL Frontend: PVL

Comments

@wandernauta
Copy link
Contributor

The following class is accepted by javac, but causes the VerCors monomorphizeClass rewrite to recurse forever:

class A<T> {
    A<A<T>> walker;
}

VerCors appears to hang until it crashes with a stack overflow exception. The same occurs when the snippet is parsed as PVL.

It's probably unlikely that someone would actually need or write such a class, but I would still not expect VerCors to get stuck - instead, I would expect an error message explaining that the class can not be monomorphized.

@bobismijnnaam bobismijnnaam added A-Bug F-Java Frontend: Java F-PVL Frontend: PVL labels Nov 19, 2024
@bobismijnnaam
Copy link
Contributor

I agree with your conclusion. Not sure if the added complexity of the check is proportional to the benefit of a nice error message, though... (Given the rarity of using generics like this)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
A-Bug F-Java Frontend: Java F-PVL Frontend: PVL
Projects
None yet
Development

No branches or pull requests

2 participants