#100 literals in switch label not deemed literal (order matters)

[David Cok]

JML Bug 1101333 is really an MJ compiler bug. Running mjc on the
same example sources produces the same incorrect behavior.

[Gary T. Leavens]

Logged In: YES
user_id=633675

I'm copying the text of the jml bug report here, and
closing that bug report.

Given these two classes (in separate files):

Switch.java:
public class Switch {
public final static int A = SwitchT.B + 1;

public int m(int i) {
switch (i) {
case A: return 0;
}
return 0;
}
}

SwitchT.java:
public class SwitchT {

public final static int B = 0;
}

The command

jml Switch.java SwitchT.java -classpath .

produces

parsing Switch.java
parsing SwitchT.java
typechecking Switch.java
File "Switch.java", line 6, character 17 error: Switch
label must be
constant value [JLS 14.9]
typechecking SwitchT.java

If the filenames are reversed in the jml command, it
executes
properly.

The problem is that in typechecking Switch.java, when
SwitchT.B
is encountered, it is not typechecked, and consequently it
is
deemed not to be a literal, hence A is not a literal and
the error
message is produced. I suspect a call of typecheck is
missing in
JClassFieldExpression.typecheck (prior to the call of
isConstant) ,
but I don't know if it was introduced by the addition of
the universe
type material.