-
Notifications
You must be signed in to change notification settings - Fork 25
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
Parser error when loading JML with nested ternary #3149
Comments
There definitely should not be an NPE. However, the type of the two arguments is different. One is \bigint the other one is int. This is how KeY got confused. |
mattulbrich
added a commit
that referenced
this issue
May 30, 2023
wadoon
added a commit
that referenced
this issue
Jun 3, 2023
* origin/main: Fix lockspec test More spammy logging removed Replace nbsp in proof script Minor changes TacletAppIndex lazy delta updates Make builtin rule app index lazy another review change optimize logging statements code review for #3152 missed a line in spotless. spotless and documentation fixing an NPE bug in the error reporting of Recoder2KeY more test cases for exceptional jml cases applying spotless improving the fix for #3149 fixes #3149 fix jacoco for gradle 8 introducing exceptional JML tests add code coverage Bump org.sonarqube from 4.0.0.2929 to 4.1.0.3113 # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeY.java
FliegendeWurst
pushed a commit
to FliegendeWurst/key
that referenced
this issue
Jun 15, 2023
Ternary operators would not have a type unless the arguments have identical types. This fix takes the promoted common type as result type. This works in particular if \bigint and int are combined.
FliegendeWurst
pushed a commit
to FliegendeWurst/key
that referenced
this issue
Jun 15, 2023
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Description
When trying to load a file (Ternary.java) where the following nested ternary expression is used within JML, KeY opens a window titled "Parser Error" with the message "null at .../Ternary.java:2:30 Caused by: java.lang.NullPointerException" and marks
true
as the problem:However, this should be valid Java Syntax – when replacing
//@ ensures \result == (((true ? (0 + 1) : 2) > 3) ? 4 : 5);
with
//@ ensures \result == 5;
in Ternary.java so that now only the Java Code contains the same ternary expression, the file becomes loadable andfoo
provable.Note: The problem seems to occur only with this specific nesting of ternary operators and a simple expression. It does NOT occur e.g. when omitting
0 +
, when using only one ternary operator or when putting the second ternary operator in place of the4
(resulting in((6 > 3) ? (true ? (0 + 1) : 2) : 5)
) or the5
.Reproducible
always
Steps to reproduce
5
The file should be loadable and
foo
provable with the use of the nested ternary operator in JML – 2. should not occur.File: Ternary.java.zip
Additional information
The "Parser Error" window contains the message
"Show Details" gives the following stacktrace:
The text was updated successfully, but these errors were encountered: