You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.";
};
The text was updated successfully, but these errors were encountered:
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.
Perhaps easiest to show by example. Right now,
examples/java/staticfield.saw
looks like this: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):
The text was updated successfully, but these errors were encountered: