User-defined sorts cannot be referenced in quantified expressions

Open mattulbrich opened this issue 1 year ago • 1 comments

Description

User-defined/Built-in KeY sorts are supposed to be accessible from within JML using a \dl_ escape. However, this does not work within quantified expressions.

Steps to reproduce

always

final class C {
	//@ invariant (\forall \dl_Seq c; c == c);
}

does not load in KeY.

Commit: 7fe4e7dba53801c38716889cec9241488ce31680

Feb 12 '24 12:02 mattulbrich

And they cannot be used in cast expressions either. (\dl_Seq)x reportedly tends to fail, too.

Feb 19 '24 13:02 mattulbrich