vdmj icon indicating copy to clipboard operation
vdmj copied to clipboard

Simple infinite type definitions cause stack overflow

Open nickbattle opened this issue 4 years ago • 0 comments

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.

nickbattle avatar Feb 22 '21 13:02 nickbattle