Description
A constant inherited by a subclass and named through it (JPEGImageWriteParam.MODE_EXPLICIT, defined in ImageWriteParam) is not resolved, and even correct code fails with a sort error. Naming it through the declaring class (ImageWriteParam.MODE_EXPLICIT) works.
Minimal reproducer
Repro.java:
import javax.imageio.ImageIO;
import javax.imageio.ImageWriteParam;
import javax.imageio.plugins.jpeg.JPEGImageWriteParam;
public class Repro {
public static void main(String[] args) {
ImageWriteParam p = ImageIO.getImageWritersByFormatName("jpeg").next().getDefaultWriteParam();
p.setCompressionMode(JPEGImageWriteParam.MODE_EXPLICIT); // same constant, inherited
p.setCompressionQuality(0.5f);
}
}ImageWriteParamRefinements.java (same directory):
import liquidjava.specification.ExternalRefinementsFor;
import liquidjava.specification.Refinement;
import liquidjava.specification.StateRefinement;
import liquidjava.specification.StateSet;
@StateSet({"start", "explicit"})
@ExternalRefinementsFor("javax.imageio.ImageWriteParam")
public interface ImageWriteParamRefinements {
@StateRefinement(to = "mode == 2 ? explicit(this) : start(this)")
void setCompressionMode(@Refinement("_ >= 0 && _ <= 3") int mode);
@StateRefinement(from = "explicit(this)")
void setCompressionQuality(@Refinement("_ >= 0.0 && _ <= 1.0") float quality);
}Expected
Correct! Passed Verification. (JPEGImageWriteParam.MODE_EXPLICIT == ImageWriteParam.MODE_EXPLICIT == 2).
Actual
Running LiquidJava on: <repro dir>
Error: Sorts Int and Bool are incompatible
6 | public static void main(String[] args) {
7 | ImageWriteParam p = ImageIO.getImageWritersByFormatName("jpeg").next().getDefaultWriteParam();
8 | p.setCompressionMode(JPEGImageWriteParam.MODE_EXPLICIT); // same constant, inherited
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
9 | p.setCompressionQuality(0.5f);
10 | }
Reproduced on main at 8816186 (liquidjava-verifier 0.0.35), and on 0.0.33.
Context
Found while turning real open-source Java code into study examples for the error-message study: real code hits this constantly, so the examples have to be rewritten around it or cannot be verified. Lower priority: real code often names the constant through the concrete class it has in mind.
Description
A constant inherited by a subclass and named through it (
JPEGImageWriteParam.MODE_EXPLICIT, defined inImageWriteParam) is not resolved, and even correct code fails with a sort error. Naming it through the declaring class (ImageWriteParam.MODE_EXPLICIT) works.Minimal reproducer
Repro.java:ImageWriteParamRefinements.java(same directory):Expected
Correct! Passed Verification.(JPEGImageWriteParam.MODE_EXPLICIT == ImageWriteParam.MODE_EXPLICIT == 2).Actual
Reproduced on
mainat 8816186 (liquidjava-verifier 0.0.35), and on 0.0.33.Context
Found while turning real open-source Java code into study examples for the error-message study: real code hits this constantly, so the examples have to be rewritten around it or cannot be verified. Lower priority: real code often names the constant through the concrete class it has in mind.