Open FliegendeWurst opened 5 months ago
Try to load the file below. It contains a syntax error (== instead of = in the problem statement), but the error message produced by KeY is bad:
==
=
line 1:1 mismatched input '5' expecting {\, '\sorts', '\schemaVariables', '\programVariables', '\include', '\includeLDTs', '\classpath', '\bootclasspath', '\javaSource', '\withOptions', '\optionsDecl', '\settings', '\profile', '\heuristicsDecl', '\predicates', '\functions', '\datatypes', '\transformers', '\rules', '\axioms', '\problem', '\chooseContract', '\proofObligation', '\proof', '\contracts', '\invariants', '/*!'}
The issue occurs because the stream is not reset to the start of the file after trying the parsing process again in non-SLL mode.
testing.key:
\functions { int b; } \problem { (\exists int c; c == 5 && c < b) & (\exists int c; c = 7 && c > b) -> b == 6 }
always
Expected behaviour: reasonable error message Actual behaviour: stupid error message (see above)
Description
Try to load the file below. It contains a syntax error (
==instead of=in the problem statement), but the error message produced by KeY is bad:line 1:1 mismatched input '5' expecting {\, '\sorts', '\schemaVariables', '\programVariables', '\include', '\includeLDTs', '\classpath', '\bootclasspath', '\javaSource', '\withOptions', '\optionsDecl', '\settings', '\profile', '\heuristicsDecl', '\predicates', '\functions', '\datatypes', '\transformers', '\rules', '\axioms', '\problem', '\chooseContract', '\proofObligation', '\proof', '\contracts', '\invariants', '/*!'}
The issue occurs because the stream is not reset to the start of the file after trying the parsing process again in non-SLL mode.
testing.key:
Reproducible
always
Steps to reproduce
Expected behaviour: reasonable error message Actual behaviour: stupid error message (see above)
Additional information