vdmj
vdmj copied to clipboard
Simple infinite type definitions cause stack overflow
The following produces a stack overflow:
types
T = R;
R = T;
Parsed 1 module in 0.054 secs. No syntax errors
java.lang.StackOverflowError
Error 3050: Type 'T' is infinite in 'DEFAULT' (test.vdm) at line 2:5
Type checked 1 module in 0.271 secs. Found 2 type errors
Although the type checker knows that T is infinite, the underlying type for R is resolved by the resolution of T, and so it does not realise that it is also infinite because the type of R is not resolved back to R (a loop). The stack overflow occurs in the type checking, where it tries to determine whether the type of T is a union, which shuttles between R and T forever.
It's tricky to fix. I suspect the infinity flag will have to be held by types rather than type definitions.