Static member names should be resolvable based on the current class

[acfoltzer]

Perhaps easiest to show by example. Right now, examples/java/staticfield.saw looks like this:

let setx_spec : JavaSetup () = do {
    newx <- java_var "newx" java_int;
    java_var "sfield.StaticField.x" java_int;
    java_ensure_eq "sfield.StaticField.x" {{ newx : [32] }};
    java_verify_tactic abc;
};

let getx_spec : JavaSetup () = do {
    x <- java_var "sfield.StaticField.x" java_int;
    java_return {{ x : [32] }};
    java_verify_tactic abc;
};

let main : TopLevel () = do {
    c <- java_load_class "sfield.StaticField";
    ms_setx <- java_verify c "setx" [] setx_spec;
    ms_getx <- java_verify c "getx" [] getx_spec;
    print "Done.";
};

Since we're running the JavaSetup blocks in the context of a class, we should be able to do so unqualified: "sfield.StaticField.x" becomes "StaticField.x" or even "x". The first alternative more accurately reflects how static references tend to appear in the text of Java programs, but one can refer to static members totally unqualified from within the same class, so we should allow that too.

Acceptance test: the following should work identically to the above script (intentionally mixing all three reference styles):

let setx_spec : JavaSetup () = do {
    newx <- java_var "newx" java_int;
    java_var "StaticField.x" java_int;
    java_ensure_eq "x" {{ newx : [32] }};
    java_verify_tactic abc;
};

let getx_spec : JavaSetup () = do {
    x <- java_var "sfield.StaticField.x" java_int;
    java_return {{ x : [32] }};
    java_verify_tactic abc;
};

let main : TopLevel () = do {
    c <- java_load_class "sfield.StaticField";
    ms_setx <- java_verify c "setx" [] setx_spec;
    ms_getx <- java_verify c "getx" [] getx_spec;
    print "Done.";
};

[brianhuffman]

The old java_verify, java_var and related commands are set to be removed soon after having been deprecated (#1005). As of #981 we can specify static fields for jvm_verify using jvm_static_field_is, and it already allows for unqualified field names when referring to static fields in the class whose method is being verified.