@Override
public native String toString();
+ @Override
+ public native boolean equals(Object o);
+
+ @Override
+ public native int hashCode();
+
/***
public String toString() {
StringBuilder sb = new StringBuilder();
// for Annotations - return the default value of the annotation member
// represented by this method
- public Object getDefaultValue() {
- throw new UnsupportedOperationException("Method.getDefaultValue() not supported yet");
- }
+ public native Object getDefaultValue();
@Override
public native boolean equals (Object obj);
package gov.nasa.jpf.jvm;
-import gov.nasa.jpf.jvm.JVMByteCodeReader;
-import gov.nasa.jpf.vm.ClassParseException;
+import java.io.File;
+
import gov.nasa.jpf.JPFException;
import gov.nasa.jpf.util.BailOut;
import gov.nasa.jpf.util.BinaryClassSource;
-
-import java.io.File;
+import gov.nasa.jpf.vm.ClassParseException;
/**
* class to read and dissect Java classfile contents (as specified by the Java VM
reader.setAnnotationCount( this, tag, annotationCount);
pos = p;
}
- private void setAnnotation(ClassFileReader reader, Object tag, int annotationIndex, String annotationType){
+ private boolean setAnnotation(ClassFileReader reader, Object tag, int annotationIndex, String annotationType){
int p = pos;
- reader.setAnnotation( this, tag, annotationIndex, annotationType);
- pos = p;
+ try {
+ reader.setAnnotation( this, tag, annotationIndex, annotationType);
+ pos = p;
+ return true;
+ } catch (SkipAnnotation sa) {
+ this.skipAnnotation(false);
+ return false;
+ }
+ }
+
+ /*
+ * This is largely lifted from AnnotationParser.java
+ * annotation {
+ * u2 type_index;
+ * u2 num_element_value_pairs;
+ * {
+ * u2 element_name_index;
+ * element_value value;
+ * } element_value_pairs[num_element_value_pairs]
+ * }
+ */
+ private void skipAnnotation(boolean skipTypeIndex) {
+ if(skipTypeIndex) { // we may want to skip after reading the type name
+ readU2();
+ }
+ int numKV = readU2();
+ for(int i = 0; i < numKV; i++) {
+ readU2(); // skip name
+ skipMemberValue();
+ }
+ }
+
+ /*
+ * Skips an element_value
+ */
+ private void skipMemberValue() {
+ int tag = readUByte();
+ switch(tag) {
+ case 'e': // Enum value
+ pos += 4; // an enum value is a struct of two shorts, for 4 bytes total
+ break;
+ case '@':
+ skipAnnotation(true);
+ break;
+ case '[':
+ skipArray();
+ break;
+ default:
+ pos += 2; // either two bye const val index or two byte class info index
+ }
}
+
+ private void skipArray() {
+ int len = readU2();
+ for(int i = 0; i < len; i++) {
+ skipMemberValue();
+ }
+ }
+
private void setAnnotationsDone(ClassFileReader reader, Object tag){
int p = pos;
reader.setAnnotationsDone(this, tag);
reader.setClassAnnotationValue( this, tag, annotationIndex, valueIndex, elementName, arrayIndex, typeName);
pos = p;
}
+
+ private void setAnnotationFieldValue(ClassFileReader reader, Object tag, int annotationIndex, int valueIndex, String elementName, int arrayIndex) {
+ int p = pos;
+ reader.setAnnotationFieldValue( this, tag, annotationIndex, valueIndex, elementName, arrayIndex);
+ pos = p;
+ }
+
private void setEnumAnnotationValue(ClassFileReader reader, Object tag, int annotationIndex, int valueIndex,
String elementName, int arrayIndex, String enumType, String enumValue){
int p = pos;
reader.setParameterAnnotationCount(this, tag, paramIndex, annotationCount);
pos = p;
}
- private void setParameterAnnotation(ClassFileReader reader, Object tag, int annotationIndex, String annotationType){
+
+ private boolean setParameterAnnotation(ClassFileReader reader, Object tag, int annotationIndex, String annotationType){
int p = pos;
- reader.setParameterAnnotation( this, tag, annotationIndex, annotationType);
- pos = p;
+ try {
+ reader.setParameterAnnotation( this, tag, annotationIndex, annotationType);
+ pos = p;
+ return true;
+ } catch(SkipAnnotation s) {
+ this.skipAnnotation(false);
+ return false;
+ }
}
private void setParameterAnnotationsDone(ClassFileReader reader, Object tag, int paramIndex){
int p = pos;
break;
case '@':
- parseAnnotation(reader, tag, 0, false); // getting recursive here
+ parseAnnotation(reader, tag, -1, false); // getting recursive here
+ setAnnotationFieldValue(reader, tag, annotationIndex, valueIndex, elementName, arrayIndex);
break;
case '[':
void parseAnnotation (ClassFileReader reader, Object tag, int annotationIndex, boolean isParameterAnnotation){
int cpIdx = readU2();
String annotationType = (String)cpValue[cpIdx];
-
+ boolean parseValues;
if (isParameterAnnotation){
- setParameterAnnotation(reader, tag, annotationIndex, annotationType);
+ parseValues = setParameterAnnotation(reader, tag, annotationIndex, annotationType);
} else {
- setAnnotation(reader, tag, annotationIndex, annotationType);
+ parseValues = setAnnotation(reader, tag, annotationIndex, annotationType);
+ }
+ if(parseValues) {
+ parseAnnotationValues(reader, tag, annotationIndex);
}
-
- parseAnnotationValues(reader, tag, annotationIndex);
}
void parseAnnotationValues (ClassFileReader reader, Object tag, int annotationIndex){
package gov.nasa.jpf.jvm;
-import gov.nasa.jpf.jvm.JVMByteCodePrinter;
+import java.io.PrintWriter;
+
import gov.nasa.jpf.util.StructuredPrinter;
import gov.nasa.jpf.vm.ClassParseException;
-import java.io.PrintWriter;
/**
* simple tool to print contents of a classfile
pw.print("..");
}
}
+
+ @Override
+ public void setAnnotationFieldValue(ClassFile cf, Object tag, int annotationIndex, int valueIndex, String elementName, int arrayIndex) {
+
+ }
}
void setAnnotationValueCount(ClassFile cf, Object tag, int annotationIndex, int nValuePairs);
void setPrimitiveAnnotationValue(ClassFile cf, Object tag, int annotationIndex, int valueIndex, String elementName, int arrayIndex, Object val);
+
+ void setAnnotationFieldValue(ClassFile cf, Object tag, int annotationIndex, int valueIndex, String elementName, int arrayIndex);
void setStringAnnotationValue(ClassFile cf, Object tag, int annotationIndex, int valueIndex, String elementName, int arrayIndex, String s);
@Override
public void setSignature(ClassFile cf, Object tag, String signature) {}
+
+ @Override
+ public void setAnnotationFieldValue(ClassFile cf, Object tag, int annotationIndex, int valueIndex, String elementName, int arrayIndex) {}
}
*/
package gov.nasa.jpf.jvm;
+import java.util.LinkedList;
+
import gov.nasa.jpf.JPFException;
import gov.nasa.jpf.vm.AnnotationInfo;
import gov.nasa.jpf.vm.AnnotationParser;
String annotationName;
AnnotationInfo.Entry[] entries;
+ protected LinkedList<AnnotationInfo> annotationStack;
+ protected AnnotationInfo curAi;
+ protected LinkedList<Object[]> valuesStack;
+
public JVMAnnotationParser (ClassFile cf) {
this.cf = cf;
}
@Override
public void setAnnotation (ClassFile cf, Object tag, int annotationIndex, String annotationType) {
- if (annotationType.equals("Ljava/lang/annotation/Inherited;")) {
+ if (key == null && annotationType.equals("Ljava/lang/annotation/Inherited;")) {
ai.setInherited( true);
}
+ if(key != null && annotationIndex == -1) {
+ if(annotationStack == null) {
+ assert valuesStack == null;
+ annotationStack = new LinkedList<>();
+ valuesStack = new LinkedList<>();
+ }
+ annotationStack.addFirst(curAi);
+ valuesStack.addFirst(valElements);
+ valElements = null;
+ curAi = ai.getClassLoaderInfo().getResolvedAnnotationInfo(Types.getClassNameFromTypeName(annotationType));
+ }
}
-
+
+ @Override
+ public void setAnnotationFieldValue(ClassFile cf, Object tag, int annotationIndex, int valueIndex, String elementName, int arrayIndex) {
+ assert annotationStack.size() > 0;
+ AnnotationInfo ai = curAi;
+ valElements = valuesStack.pop();
+ curAi = annotationStack.pop();
+ if(arrayIndex >= 0) {
+ valElements[arrayIndex] = ai;
+ } else {
+ if(curAi != null) {
+ curAi.setClonedEntryValue(elementName, ai);
+ } else {
+ value = ai;
+ }
+ }
+ }
+
@Override
public void setPrimitiveAnnotationValue (ClassFile cf, Object tag, int annotationIndex, int valueIndex,
String elementName, int arrayIndex, Object val) {
if (arrayIndex >= 0) {
valElements[arrayIndex] = val;
+ } else if(curAi != null) {
+ curAi.setClonedEntryValue(elementName, val);
} else {
if (key != null){
value = val;
}
}
}
-
+
@Override
public void setStringAnnotationValue (ClassFile cf, Object tag, int annotationIndex, int valueIndex,
String elementName, int arrayIndex, String val) {
if (arrayIndex >= 0) {
valElements[arrayIndex] = val;
+ } else if(curAi != null) {
+ curAi.setClonedEntryValue(elementName, val);
} else {
if (key != null){
value = val;
Object val = AnnotationInfo.getClassValue(typeName);
if (arrayIndex >= 0) {
valElements[arrayIndex] = val;
+ } else if(curAi != null) {
+ curAi.setClonedEntryValue(elementName, val);
} else {
if (key != null){
value = val;
Object val = AnnotationInfo.getEnumValue(enumType, enumValue);
if (arrayIndex >= 0) {
valElements[arrayIndex] = val;
+ } else if(curAi != null) {
+ curAi.setClonedEntryValue(elementName, val);
} else {
if (key != null){
value = val;
@Override
public void setAnnotationValueElementsDone (ClassFile cf, Object tag, int annotationIndex, int valueIndex,
String elementName) {
- if (key != null) {
+ if(curAi != null) {
+ curAi.setClonedEntryValue(elementName, valElements);
+ } else if (key != null) {
value = valElements;
}
}
package gov.nasa.jpf.jvm;
-import gov.nasa.jpf.Config;
-import gov.nasa.jpf.util.Misc;
-import gov.nasa.jpf.util.StringSetMatcher;
-import gov.nasa.jpf.vm.*;
-
import java.lang.reflect.Modifier;
import java.util.HashMap;
import java.util.LinkedHashMap;
+import java.util.LinkedList;
+
+import gov.nasa.jpf.Config;
+import gov.nasa.jpf.util.Misc;
+import gov.nasa.jpf.util.StringSetMatcher;
+import gov.nasa.jpf.vm.AbstractTypeAnnotationInfo;
+import gov.nasa.jpf.vm.AnnotationInfo;
+import gov.nasa.jpf.vm.BootstrapMethodInfo;
+import gov.nasa.jpf.vm.BytecodeAnnotationInfo;
+import gov.nasa.jpf.vm.BytecodeTypeParameterAnnotationInfo;
+import gov.nasa.jpf.vm.ClassInfo;
+import gov.nasa.jpf.vm.ClassInfoException;
+import gov.nasa.jpf.vm.ClassLoaderInfo;
+import gov.nasa.jpf.vm.ClassParseException;
+import gov.nasa.jpf.vm.DirectCallStackFrame;
+import gov.nasa.jpf.vm.ExceptionHandler;
+import gov.nasa.jpf.vm.ExceptionParameterAnnotationInfo;
+import gov.nasa.jpf.vm.FieldInfo;
+import gov.nasa.jpf.vm.FormalParameterAnnotationInfo;
+import gov.nasa.jpf.vm.GenericSignatureHolder;
+import gov.nasa.jpf.vm.InfoObject;
+import gov.nasa.jpf.vm.LocalVarInfo;
+import gov.nasa.jpf.vm.MethodInfo;
+import gov.nasa.jpf.vm.NativeMethodInfo;
+import gov.nasa.jpf.vm.StackFrame;
+import gov.nasa.jpf.vm.SuperTypeAnnotationInfo;
+import gov.nasa.jpf.vm.ThreadInfo;
+import gov.nasa.jpf.vm.ThrowsAnnotationInfo;
+import gov.nasa.jpf.vm.TypeAnnotationInfo;
+import gov.nasa.jpf.vm.TypeParameterAnnotationInfo;
+import gov.nasa.jpf.vm.TypeParameterBoundAnnotationInfo;
+import gov.nasa.jpf.vm.Types;
+import gov.nasa.jpf.vm.VariableAnnotationInfo;
/**
* a ClassInfo that was created from a Java classfile
//--- annotations
protected AnnotationInfo[] annotations;
protected AnnotationInfo curAi;
+ protected LinkedList<AnnotationInfo> annotationStack;
+ protected LinkedList<Object[]> valuesStack;
protected AnnotationInfo[][] parameterAnnotations;
protected Object[] values;
+ // true if we need to filter null annotations
+ private boolean compactAnnotationArray = false;
//--- declaration annotations
@Override
public void setAnnotation (ClassFile cf, Object tag, int annotationIndex, String annotationType) {
if (tag instanceof InfoObject) {
- curAi = getResolvedAnnotationInfo(Types.getClassNameFromTypeName(annotationType));
- annotations[annotationIndex] = curAi;
+ if(annotationIndex == -1) {
+ if(annotationStack == null) {
+ assert valuesStack == null;
+ valuesStack = new LinkedList<>();
+ annotationStack = new LinkedList<>();
+ }
+ annotationStack.addFirst(curAi);
+ valuesStack.addFirst(values);
+ }
+ try {
+ curAi = getResolvedAnnotationInfo(Types.getClassNameFromTypeName(annotationType));
+ if(annotationIndex != -1) {
+ annotations[annotationIndex] = curAi;
+ }
+ } catch(ClassInfoException cie) {
+ // if we can't parse a field, we're sunk, throw and tank the reflective call
+ if(annotationIndex == -1) {
+ throw cie;
+ }
+ compactAnnotationArray = true;
+ annotations[annotationIndex] = null;
+ // skip this annotation
+ throw new SkipAnnotation();
+ }
}
}
@Override
public void setAnnotationsDone (ClassFile cf, Object tag) {
if (tag instanceof InfoObject) {
- ((InfoObject) tag).addAnnotations(annotations);
+ AnnotationInfo[] toSet;
+ if(compactAnnotationArray) {
+ int nAnnot = 0;
+ for(AnnotationInfo ai : annotations) {
+ if(ai != null) {
+ nAnnot++;
+ }
+ }
+ toSet = new AnnotationInfo[nAnnot];
+ int idx = 0;
+ for(AnnotationInfo ai : annotations) {
+ if(ai != null) {
+ toSet[idx++] = ai;
+ }
+ }
+ } else {
+ toSet = annotations;
+ }
+ ((InfoObject) tag).addAnnotations(toSet);
}
+ compactAnnotationArray = false;
}
@Override
@Override
public void setParameterAnnotation (ClassFile cf, Object tag, int annotationIndex, String annotationType) {
- curAi = getResolvedAnnotationInfo(Types.getClassNameFromTypeName(annotationType));
- annotations[annotationIndex] = curAi;
+ try {
+ curAi = getResolvedAnnotationInfo(Types.getClassNameFromTypeName(annotationType));
+ annotations[annotationIndex] = curAi;
+ } catch(ClassInfoException cie) {
+ compactAnnotationArray = true;
+ annotations[annotationIndex] = null;
+ throw new SkipAnnotation();
+ }
}
@Override
public void setAnnotationValueCount (ClassFile cf, Object tag, int annotationIndex, int nValuePairs) {
// if we have values, we need to clone the defined annotation so that we can overwrite entries
curAi = curAi.cloneForOverriddenValues();
- annotations[annotationIndex] = curAi;
+ if(annotationIndex != -1) {
+ annotations[annotationIndex] = curAi;
+ }
}
@Override
curAi.setClonedEntryValue(elementName, val);
}
}
+
+ @Override
+ public void setAnnotationFieldValue(ClassFile cf, Object tag, int annotationIndex, int valueIndex, String elementName, int arrayIndex) {
+ assert annotationStack.size() > 0;
+ AnnotationInfo ai = curAi;
+ values = valuesStack.pop();
+ curAi = annotationStack.pop();
+ if(arrayIndex >= 0) {
+ values[arrayIndex] = ai;
+ } else {
+ curAi.setClonedEntryValue(elementName, ai);
+ }
+ }
@Override
public void setStringAnnotationValue (ClassFile cf, Object tag, int annotationIndex, int valueIndex,
--- /dev/null
+package gov.nasa.jpf.jvm;
+
+public class SkipAnnotation extends RuntimeException {
+
+}
*/
package gov.nasa.jpf.vm;
-import com.sun.org.apache.bcel.internal.generic.InstructionConstants;
+import java.util.Date;
+import java.util.Locale;
+import java.util.Optional;
+
import gov.nasa.jpf.Config;
import gov.nasa.jpf.JPF;
import gov.nasa.jpf.JPFException;
import gov.nasa.jpf.JPFListener;
+import gov.nasa.jpf.vm.AnnotationInfo.EnumValue;
import gov.nasa.jpf.vm.serialize.UnknownJPFClass;
-import java.util.Date;
-import java.util.Locale;
-
-
/**
* MJIEnv is the call environment for "native" methods, i.e. code that
* is executed by the VM, not by JPF.
}
}
}
-
return String.format(format,arg);
}
public void throwException (String clsName) {
ClassInfo ciX = ClassInfo.getInitializedClassInfo(clsName, ti);
- assert ciX.isInstanceOf("java.lang.Throwable");
+ assert ciX.isInstanceOf("java.lang.Throwable") : ciX;
exceptionRef = ti.createException(ciX, null, NULL);
}
ElementInfo ei = getModifiableElementInfo(objref);
ei.lockNotified(ti);
}
-
- void initAnnotationProxyField (int proxyRef, FieldInfo fi, Object v) throws ClinitRequired {
- String fname = fi.getName();
- String ftype = fi.getType();
-
+
+ public int liftNativeAnnotationValue(String ftype, Object v) {
if (v instanceof String){
- setReferenceField(proxyRef, fname, newString((String)v));
+ return newString((String)v);
} else if (v instanceof Boolean){
- setBooleanField(proxyRef, fname, ((Boolean)v).booleanValue());
- } else if (v instanceof Integer){
- setIntField(proxyRef, fname, ((Integer)v).intValue());
+ return valueOfBoolean((Boolean)v);
+ } else if (v instanceof Integer) {
+ return valueOfInteger((Integer)v);
} else if (v instanceof Long){
- setLongField(proxyRef, fname, ((Long)v).longValue());
+ return valueOfLong((Long)v);
} else if (v instanceof Float){
- setFloatField(proxyRef, fname, ((Float)v).floatValue());
+ return newFloat((Float) v);
} else if (v instanceof Short){
- setShortField(proxyRef, fname, ((Short)v).shortValue());
+ return valueOfShort((Short)v);
} else if (v instanceof Character){
- setCharField(proxyRef, fname, ((Character)v).charValue());
+ return valueOfCharacter((Character)v);
} else if (v instanceof Byte){
- setByteField(proxyRef, fname, ((Byte)v).byteValue());
+ return valueOfByte((Byte)v);
} else if (v instanceof Double){
- setDoubleField(proxyRef, fname, ((Double)v).doubleValue());
-
- } else if (v instanceof AnnotationInfo.EnumValue){ // an enum constant
- AnnotationInfo.EnumValue ev = (AnnotationInfo.EnumValue)v;
- String eCls = ev.getEnumClassName();
- String eConst = ev.getEnumConstName();
-
- ClassInfo eci = ClassLoaderInfo.getCurrentResolvedClassInfo(eCls);
- if (!eci.isInitialized()){
- throw new ClinitRequired(eci);
+ return newDouble((Double)v);
+ } else {
+ Optional<Integer> ref = liftAnnotationReferenceValue(v, ftype);
+ if(ref.isPresent()) {
+ return ref.get();
+ } else {
+ throwException("java.lang.InternalError", "AnnotationElement type not supported: " + ftype);
+ return -1;
}
-
- StaticElementInfo sei = eci.getStaticElementInfo();
- int eref = sei.getReferenceField(eConst);
- setReferenceField(proxyRef, fname, eref);
+ }
+ }
+
+ Optional<Integer> liftAnnotationReferenceValue(Object v, String ftype) {
+ if (v instanceof AnnotationInfo.EnumValue){ // an enum constant
+ int eref = makeAnnotationEnumRef((EnumValue) v);
+ return Optional.of(eref);
} else if (v instanceof AnnotationInfo.ClassValue){ // a class
String clsName = v.toString();
}
int cref = cci.getClassObjectRef();
- setReferenceField(proxyRef, fname, cref);
+ return Optional.of(cref);
} else if (v.getClass().isArray()){ // ..or arrays thereof
Object[] a = (Object[])v;
for (int i=0; i<a.length; i++){
setDoubleArrayElement(aref,i,((Number)a[i]).doubleValue());
}
+ } else if(ftype.equals("char[]")) {
+ aref = newCharArray(a.length);
+ for (int i=0; i<a.length; i++){
+ setCharArrayElement(aref,i,((Character)a[i]).charValue());
+ }
+ } else if(ftype.equals("short[]")) {
+ aref = newShortArray(a.length);
+ for (int i=0; i<a.length; i++){
+ setShortArrayElement(aref,i,((Number)a[i]).shortValue());
+ }
+ } else if(ftype.equals("byte[]")) {
+ aref = newByteArray(a.length);
+ for (int i=0; i<a.length; i++){
+ setByteArrayElement(aref,i,((Number)a[i]).byteValue());
+ }
+ } else if(ftype.equals("float[]")) {
+ aref = newFloatArray(a.length);
+ for (int i=0; i<a.length; i++){
+ setFloatArrayElement(aref,i,((Number)a[i]).floatValue());
+ }
} else if (ftype.equals("java.lang.Class[]")){
aref = newObjectArray("java.lang.Class", a.length);
for (int i=0; i<a.length; i++){
int cref = cci.getClassObjectRef();
setReferenceArrayElement(aref,i,cref);
}
+ } else {
+ String typeName = ftype.substring(0, ftype.length() - 2);
+ ClassInfo elemType = ClassLoaderInfo.getCurrentResolvedClassInfo(typeName);
+ aref = newObjectArray(typeName, a.length);
+ if(elemType.isEnum()) {
+ for(int i = 0; i < a.length; i++) {
+ setReferenceArrayElement(aref, i, makeAnnotationEnumRef((EnumValue) a[i]));
+ }
+
+ } else {
+ for(int i = 0; i < a.length; i++) {
+ setReferenceArrayElement(aref, i, makeAnnotationProxy((AnnotationInfo) a[i]));
+ }
+ }
}
if (aref != NULL){
- setReferenceField(proxyRef, fname, aref);
+ return Optional.of(aref);
} else {
- throwException("AnnotationElement type not supported: " + ftype);
+ return Optional.empty();
}
+ } else if(v instanceof AnnotationInfo) {
+ return Optional.of(makeAnnotationProxy((AnnotationInfo) v));
+ } else {
+ return Optional.empty();
+ }
+ }
+
+ void initAnnotationProxyField (int proxyRef, FieldInfo fi, Object v) throws ClinitRequired {
+ String fname = fi.getName();
+ String ftype = fi.getType();
+
+ if (v instanceof String){
+ setReferenceField(proxyRef, fname, newString((String)v));
+ } else if (v instanceof Boolean){
+ setBooleanField(proxyRef, fname, ((Boolean)v).booleanValue());
+ } else if (v instanceof Integer){
+ setIntField(proxyRef, fname, ((Integer)v).intValue());
+ } else if (v instanceof Long){
+ setLongField(proxyRef, fname, ((Long)v).longValue());
+ } else if (v instanceof Float){
+ setFloatField(proxyRef, fname, ((Float)v).floatValue());
+ } else if (v instanceof Short){
+ setShortField(proxyRef, fname, ((Short)v).shortValue());
+ } else if (v instanceof Character){
+ setCharField(proxyRef, fname, ((Character)v).charValue());
+ } else if (v instanceof Byte){
+ setByteField(proxyRef, fname, ((Byte)v).byteValue());
+ } else if (v instanceof Double){
+ setDoubleField(proxyRef, fname, ((Double)v).doubleValue());
} else {
- throwException("AnnotationElement type not supported: " + ftype);
+ Optional<Integer> ref = liftAnnotationReferenceValue(v, ftype);
+ if(ref.isPresent()) {
+ setReferenceField(proxyRef, fname, ref.get());
+ } else {
+ throwException("java.lang.InternalError", "AnnotationElement type not supported: " + ftype);
+ }
}
}
+ private int makeAnnotationEnumRef(AnnotationInfo.EnumValue v) {
+ AnnotationInfo.EnumValue ev = (AnnotationInfo.EnumValue)v;
+ String eCls = ev.getEnumClassName();
+ String eConst = ev.getEnumConstName();
+
+ ClassInfo eci = ClassLoaderInfo.getCurrentResolvedClassInfo(eCls);
+ if (!eci.isInitialized()){
+ throw new ClinitRequired(eci);
+ }
+
+ StaticElementInfo sei = eci.getStaticElementInfo();
+ int eref = sei.getReferenceField(eConst);
+ return eref;
+ }
+
int newAnnotationProxy (ClassInfo aciProxy, AnnotationInfo ai) throws ClinitRequired {
int proxyRef = newObject(aciProxy);
Object v = e.getValue();
String fname = e.getKey();
FieldInfo fi = aciProxy.getInstanceField(fname);
-
initAnnotationProxyField(proxyRef, fi, v);
}
if ((ai != null) && (ai.length > 0)){
int aref = newObjectArray("Ljava/lang/annotation/Annotation;", ai.length);
for (int i=0; i<ai.length; i++){
- ClassInfo aci = ClassLoaderInfo.getCurrentResolvedClassInfo(ai[i].getName());
- ClassInfo aciProxy = aci.getAnnotationProxy();
-
- int ar = newAnnotationProxy(aciProxy, ai[i]);
+ int ar = makeAnnotationProxy(ai[i]);
setReferenceArrayElement(aref, i, ar);
}
return aref;
}
}
+ private int makeAnnotationProxy(AnnotationInfo annotationInfo) {
+ ClassInfo aci = ClassLoaderInfo.getCurrentResolvedClassInfo(annotationInfo.getName());
+ ClassInfo aciProxy = aci.getAnnotationProxy();
+
+ int ar = newAnnotationProxy(aciProxy, annotationInfo);
+ return ar;
+ }
+
public void handleClinitRequest (ClassInfo ci) {
ThreadInfo ti = getThreadInfo();
package gov.nasa.jpf.vm;
+import java.util.Arrays;
+import java.util.Objects;
+import java.util.function.IntFunction;
+
import gov.nasa.jpf.annotation.MJI;
/**
return ci.getClassObjectRef();
}
+ @MJI
+ public boolean equals__Ljava_lang_Object_2__Z(MJIEnv env, int objRef, int otherObj) {
+ if(otherObj == MJIEnv.NULL) {
+ return false;
+ }
+ ClassInfo thisProxy = env.getClassInfo(objRef);
+ ClassInfo otherProxy = env.getClassInfo(otherObj);
+ if(!thisProxy.equals(otherProxy)) {
+ if(!otherProxy.getAllInterfaceClassInfos().containsAll(thisProxy.getAllInterfaces())) {
+ return false;
+ }
+ // oof, someone implemented an annotation in user code. Delegate to their equals and let them deal with it
+ MethodInfo mi = otherProxy.getMethod("equals(Ljava/lang/Object;)Z", true);
+ assert mi != null;
+ ThreadInfo ti = env.getThreadInfo();
+ DirectCallStackFrame frame = ti.getReturnedDirectCall();
+ if(frame == null) {
+ frame = mi.createDirectCallStackFrame(ti, 0);
+ frame.setReferenceArgument(0, otherObj, env.getObjectAttr(otherObj));
+ frame.setReferenceArgument(1, objRef, env.getObjectAttr(objRef));
+ ti.pushFrame(frame);
+ return false;
+ } else {
+ Object attr = frame.getResultAttr();
+ int ret = frame.getResult();
+ env.setReturnAttribute(attr);
+ return ret == 1;
+ }
+ }
+ return annotationsEqual(env, objRef, otherObj);
+ }
+
+ public static boolean annotationsEqual(MJIEnv env, int aObj, int bObj) {
+ if((aObj == MJIEnv.NULL) != (bObj == MJIEnv.NULL)) {
+ return false;
+ }
+ ClassInfo thisProxy = env.getClassInfo(aObj);
+ ClassInfo otherProxy = env.getClassInfo(bObj);
+ if(!thisProxy.equals(otherProxy)) {
+ return false;
+ }
+ FieldInfo[] fields = thisProxy.getDeclaredInstanceFields();
+ ElementInfo aE = env.getElementInfo(aObj);
+ ElementInfo bE = env.getElementInfo(bObj);
+ for (int i=0; i<fields.length; i++){
+ FieldInfo fi = fields[i];
+ String fn = fi.getName();
+ String ft = fi.getType();
+ if(!fi.isReference()) {
+ if(fi.is1SlotField()) {
+ if(aE.get1SlotField(fi) != bE.get1SlotField(fi)) {
+ return false;
+ }
+ } else {
+ if(aE.get2SlotField(fi) != bE.get2SlotField(fi)) {
+ return false;
+ }
+ }
+ } else if(ft.equals("java.lang.Class")) {
+ if(env.getReferenceField(aObj, fi) != env.getReferenceField(bObj, fi)) {
+ return false;
+ }
+ } else if(ft.equals("java.lang.String")) {
+ String aStr = env.getStringField(aObj, fn);
+ String bStr = env.getStringField(bObj, fn);
+ if(!Objects.equals(aStr, bStr)) {
+ return false;
+ }
+ } else if(ft.endsWith("[]")) {
+ String elemType = Types.getTypeName(Types.getArrayElementType(fi.getSignature()));
+ int aArrayRef = env.getReferenceField(aObj, fi);
+ int bArrayRef = env.getReferenceField(bObj, fi);
+ if((aArrayRef == MJIEnv.NULL) != (bArrayRef == MJIEnv.NULL)) {
+ return false;
+ }
+ ElementInfo aArrayContents = env.getElementInfo(aArrayRef);
+ ElementInfo bArrayContents = env.getElementInfo(bArrayRef);
+ assert aArrayContents.isArray() && bArrayContents.isArray();
+ if(Types.isBasicType(elemType) || elemType.equals("java.lang.Class")) {
+ Object rawArray1 = aArrayContents.getArrayFields().getValues();
+ Object rawArray2 = bArrayContents.getArrayFields().getValues();
+ if(!Objects.deepEquals(rawArray1, rawArray2)) {
+ return false;
+ }
+ // string array
+ } else if(elemType.equals("java.lang.String")) {
+ if(!Arrays.equals(env.getStringArrayObject(aArrayRef), env.getStringArrayObject(bArrayRef))) {
+ return false;
+ }
+ // either annotation or enum
+ } else {
+ int arrayLength1 = env.getArrayLength(aArrayRef);
+ int arrayLength2 = env.getArrayLength(bArrayRef);
+ if(arrayLength2 != arrayLength1) {
+ return false;
+ }
+ for(int j = 0; j < arrayLength1; j++) {
+ int elem1Ref = env.getReferenceArrayElement(aArrayRef, j);
+ int elem2Ref = env.getReferenceArrayElement(bArrayRef, j);
+ assert elem1Ref != MJIEnv.NULL && elem2Ref != MJIEnv.NULL;
+ if(!referenceTypesEqual(env, elem1Ref, elem2Ref)) {
+ return false;
+ }
+ }
+ }
+ } else {
+ if(!referenceTypesEqual(env, env.getReferenceField(aObj, fi), env.getReferenceField(bObj, fi))) {
+ return false;
+ }
+ }
+ }
+ return true;
+ }
+
+ private static boolean referenceTypesEqual(MJIEnv env, int elem1Ref, int elem2Ref) {
+ ClassInfo aci = env.getClassInfo(elem1Ref);
+ ClassInfo bci = env.getClassInfo(elem2Ref);
+ assert aci != null && bci != null;
+ if(!aci.equals(bci)) {
+ return false;
+ }
+ if(aci.isEnum()) {
+ return elem1Ref == elem2Ref;
+ } else {
+ return annotationsEqual(env, elem1Ref, elem2Ref);
+ }
+ }
+
@MJI
public int toString____Ljava_lang_String_2 (MJIEnv env, int objref){
- StringBuffer sb = new StringBuffer();
-
+ StringBuilder sb = new StringBuilder();
+ annotationReferenceToString(env, objref, sb);
+ return env.newString(sb.toString());
+ }
+
+ private int annotationHashCode(MJIEnv env, int objRef) {
+ ClassInfo thisProxy = env.getClassInfo(objRef);
+ FieldInfo[] fields = thisProxy.getDeclaredInstanceFields();
+ int hashCode = 0;
+ for (int i=0; i<fields.length; i++){
+ FieldInfo fi = fields[i];
+ int fieldHash = computeFieldHash(env, objRef, fi);
+ hashCode += (127 * getStringHash(env, env.newString(fi.getName()))) ^ fieldHash;
+ }
+ return hashCode;
+ }
+
+ private int computeFieldHash(MJIEnv env, int objRef, FieldInfo fi) {
+ String fn = fi.getName();
+ String ft = fi.getType();
+ if(!fi.isReference()) {
+ switch(ft) {
+ case "byte":
+ return Byte.valueOf(env.getByteField(objRef, fn)).hashCode();
+ case "boolean":
+ return Boolean.valueOf(env.getBooleanField(objRef, fn)).hashCode();
+ case "char":
+ return Character.valueOf(env.getCharField(objRef, fn)).hashCode();
+ case "short":
+ return Short.valueOf(env.getShortField(objRef, fn)).hashCode();
+ case "int":
+ return Integer.valueOf(env.getIntField(objRef, fn)).hashCode();
+ case "long":
+ return Long.valueOf(env.getLongField(objRef, fn)).hashCode();
+ case "float":
+ return Float.valueOf(env.getFloatField(objRef, fn)).hashCode();
+ case "double":
+ return Double.valueOf(env.getDoubleField(objRef, fn)).hashCode();
+ default:
+ throw new UnsupportedOperationException();
+ }
+ } else if(ft.equals("java.lang.Class")) {
+ return getObjectHash(env.getReferenceField(objRef, fi));
+ } else if(ft.equals("java.lang.String")) {
+ return getStringHash(env, env.getReferenceField(objRef, fi));
+ } else if(ft.endsWith("[]")) {
+ int aArrayRef = env.getReferenceField(objRef, fi);
+ ElementInfo aArrayContents = env.getElementInfo(aArrayRef);
+ String elemType = Types.getTypeName(Types.getArrayElementType(fi.getSignature()));
+ if(Types.isBasicType(elemType)) {
+ Object rawArray1 = aArrayContents.getArrayFields().getValues();
+ if(rawArray1 instanceof boolean[]) {
+ return Arrays.hashCode((boolean[])rawArray1);
+ } else if(rawArray1 instanceof byte[]) {
+ return Arrays.hashCode((byte[])rawArray1);
+ } else if(rawArray1 instanceof char[]) {
+ return Arrays.hashCode((char[])rawArray1);
+ } else if(rawArray1 instanceof short[]) {
+ return Arrays.hashCode((short[])rawArray1);
+ } else if(rawArray1 instanceof int[]) {
+ return Arrays.hashCode((int[])rawArray1);
+ } else if(rawArray1 instanceof long[]) {
+ return Arrays.hashCode((long[])rawArray1);
+ } else if(rawArray1 instanceof float[]) {
+ return Arrays.hashCode((float[])rawArray1);
+ } else if(rawArray1 instanceof double[]) {
+ return Arrays.hashCode((double[])rawArray1);
+ } else {
+ throw new RuntimeException();
+ }
+ } else if(elemType.equals("java.lang.Class")) {
+ return computeObjectArrayHash(env, aArrayRef, this::getObjectHash);
+ // string array
+ } else if(elemType.equals("java.lang.String")) {
+ return computeObjectArrayHash(env, aArrayRef, (ref) -> getStringHash(env, ref));
+ } else {
+ return computeObjectArrayHash(env, aArrayRef, (ref) -> hashReferenceValue(env, ref));
+ }
+ } else {
+ return hashReferenceValue(env, env.getReferenceField(objRef, fi));
+ }
+ }
+
+ /*
+ * THIS WILL BREAK if the JDK uses a different hashcode from the one here
+ */
+ private int computeObjectArrayHash(MJIEnv env, int arrayRef, IntFunction<Integer> refHasher) {
+ int arrayLength1 = env.getArrayLength(arrayRef);
+ int hash = 1;
+ for(int j = 0; j < arrayLength1; j++) {
+ int elem1Ref = env.getReferenceArrayElement(arrayRef, j);
+ hash = 31 * hash + refHasher.apply(elem1Ref);
+ }
+ return hash;
+ }
+
+ private int getStringHash(MJIEnv env, int strObjRef) {
+ return JPF_java_lang_String.computeStringHashCode(env, strObjRef);
+ }
+
+ private int getObjectHash(int ref) {
+ return ref ^ 0xABCD;
+ }
+
+ private int hashReferenceValue(MJIEnv env, int elem1Ref) {
+ ClassInfo aci = env.getClassInfo(elem1Ref);
+ if(aci.isEnum()) {
+ return getObjectHash(elem1Ref);
+ } else {
+ return annotationHashCode(env, elem1Ref);
+ }
+ }
+
+ @MJI
+ public int hashCode____I(MJIEnv env, int objRef) {
+ return annotationHashCode(env, objRef);
+ }
+
+ private void annotationReferenceToString(MJIEnv env, int objref, StringBuilder sb) {
ClassInfo ci = env.getClassInfo(objref);
String cname = ci.getName();
int idx = cname.lastIndexOf('$');
sb.append(fn);
sb.append('=');
- if (ft.equals("int")){
+ if(ft.equals("int")) {
sb.append(env.getIntField(objref,fn));
- } else if (ft.equals("long")){
- sb.append(env.getLongField(objref,fn));
-
- } else if (ft.equals("double")){
- sb.append(env.getDoubleField(objref,fn));
+ } else if(ft.equals("byte")) {
+ sb.append(env.getByteField(objref,fn));
- } else if (ft.equals("boolean")){
+ } else if(ft.equals("boolean")) {
sb.append(env.getBooleanField(objref,fn));
-
- } else if (ft.equals("java.lang.String")){
+
+ } else if(ft.equals("short")) {
+ sb.append(env.getShortField(objref, fn));
+
+ } else if(ft.equals("char")) {
+ sb.append(env.getCharField(objref, fn));
+
+ } else if(ft.equals("float")) {
+ sb.append(env.getFloatField(objref, fn));
+
+ } else if(ft.equals("long")) {
+ sb.append(env.getLongField(objref, fn));
+
+ } else if(ft.equals("double")) {
+ sb.append(env.getDoubleField(objref,fn));
+
+ } else if(ft.equals("java.lang.String")) {
sb.append(env.getStringObject(env.getReferenceField(objref, fn)));
-
- } else if (ft.equals("java.lang.Class")){
+
+ } else if(ft.equals("java.lang.Class")) {
int cref = env.getReferenceField(objref, fn);
if (cref != MJIEnv.NULL){
int nref = env.getReferenceField(cref, "name");
} else {
sb.append("class ?");
}
-
- } else if (ft.endsWith("[]")){
+
+ } else if(ft.endsWith("[]")) {
int ar = env.getReferenceField(objref, fn);
int n = env.getArrayLength((ar));
sb.append('[');
-
- if (ft.equals("java.lang.String[]")){
+
+ if(ft.equals("int[]")) {
for (int j=0; j<n; j++){
if (j>0) sb.append(',');
- sb.append(env.getStringObject(env.getReferenceArrayElement(ar,j)));
+ sb.append(env.getIntArrayElement(ar,j));
}
-
- } else if (ft.equals("int[]")){
+
+ } else if(ft.equals("byte[]")) {
for (int j=0; j<n; j++){
if (j>0) sb.append(',');
- sb.append(env.getIntArrayElement(ar,j));
+ sb.append(env.getByteArrayElement(ar,j));
+ }
+
+ } else if(ft.equals("boolean[]")) {
+ for (int j=0; j<n; j++){
+ if (j>0) sb.append(',');
+ sb.append(env.getBooleanArrayElement(ar,j));
+ }
+
+ } else if(ft.equals("short[]")) {
+ for (int j=0; j<n; j++){
+ if (j>0) sb.append(',');
+ sb.append(env.getShortArrayElement(ar,j));
+ }
+
+ } else if(ft.equals("char[]")) {
+ for (int j=0; j<n; j++){
+ if (j>0) sb.append(',');
+ sb.append(env.getCharArrayElement(ar,j));
+ }
+
+ } else if(ft.equals("float[]")) {
+ for (int j=0; j<n; j++){
+ if (j>0) sb.append(',');
+ sb.append(env.getFloatArrayElement(ar,j));
}
- } else if (ft.equals("long[]")){
+ } else if(ft.equals("long[]")) {
for (int j=0; j<n; j++){
if (j>0) sb.append(',');
sb.append(env.getLongArrayElement(ar,j));
}
-
- } else if (ft.equals("double[]")){
+
+ } else if(ft.equals("double[]")) {
for (int j=0; j<n; j++){
if (j>0) sb.append(',');
sb.append(env.getDoubleArrayElement(ar,j));
}
-
- } else if (ft.equals("boolean[]")){
+
+ } else if(ft.equals("java.lang.String[]")) {
for (int j=0; j<n; j++){
if (j>0) sb.append(',');
- sb.append(env.getBooleanArrayElement(ar,j));
+ sb.append(env.getStringObject(env.getReferenceArrayElement(ar,j)));
}
- } else if (ft.equals("java.lang.Class[]")){
+
+ } else if(ft.equals("java.lang.Class[]")) {
for (int j=0; j<n; j++){
if (j>0) sb.append(',');
sb.append("class ?");
}
- }
+ }
+ } else {
+ for(int j=0; j < n; j++) {
+ if (j>0) sb.append(',');
+
+ int cref = env.getReferenceArrayElement(ar,j);
+ if (cref != MJIEnv.NULL){
+ referenceToString(env, sb, cref);
+ } else {
+ sb.append("null");
+ }
+ }
}
- sb.append(']');
-
- } else { // arbitrary type name, must be a reference
+ sb.append("]");
+ } else {
int eref = env.getReferenceField(objref, fn);
if (eref != MJIEnv.NULL){
- ClassInfo eci = env.getClassInfo(eref);
- if (eci.isEnum()){
- int nref = env.getReferenceField(eref, "name");
- String en = env.getStringObject(nref);
-
- sb.append(eci.getName());
- sb.append('.');
- sb.append(en);
- }
+ referenceToString(env, sb, eref);
}
}
}
sb.append(')');
}
-
-
- return env.newString(sb.toString());
+ }
+
+ private void referenceToString(MJIEnv env, StringBuilder sb, int eref) {
+ ClassInfo eci = env.getClassInfo(eref);
+ if (eci.isEnum()){
+ int nref = env.getReferenceField(eref, "name");
+ String en = env.getStringObject(nref);
+
+ sb.append(eci.getName());
+ sb.append('.');
+ sb.append(en);
+ } else {
+ annotationReferenceToString(env, eref, sb);
+ }
}
}
*/
package gov.nasa.jpf.vm;
-import gov.nasa.jpf.Config;
-import gov.nasa.jpf.annotation.MJI;
-
import java.io.IOException;
import java.io.InputStream;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.Set;
+import gov.nasa.jpf.Config;
+import gov.nasa.jpf.annotation.MJI;
+
/**
* MJI NativePeer class for java.lang.Class library abstraction
@MJI
public int hashCode____I (MJIEnv env, int objref) {
+ return computeStringHashCode(env, objref);
+ }
+
+ public static int computeStringHashCode(MJIEnv env, int objref) {
ElementInfo ei = env.getElementInfo(objref);
int h = ei.getIntField("hash");
return getExceptionTypes(env, getMethodInfo(env, objRef));
}
+ @MJI
+ public int getDefaultValue____Ljava_lang_Object_2(MJIEnv env, int objRef) {
+ MethodInfo mi = getMethodInfo(env, objRef);
+ ClassInfo ci = mi.getClassInfo();
+ if(!ci.isInterface() || ci.getDirectInterfaceNames() == null || ci.getDirectInterfaceNames().length != 1 || !ci.getDirectInterfaceNames()[0].equals("java.lang.annotation.Annotation")) {
+ return MJIEnv.NULL;
+ }
+ String annotationName = ci.getName();
+ AnnotationInfo ai = ci.getClassLoaderInfo().getResolvedAnnotationInfo(annotationName);
+ Object o = ai.getValue(mi.getName());
+ if(o == null) {
+ return MJIEnv.NULL;
+ }
+ try {
+ return env.liftNativeAnnotationValue(Types.getTypeName(mi.getReturnType()), o);
+ } catch(ClinitRequired e) {
+ env.handleClinitRequest(e.getRequiredClassInfo());
+ return -1;
+ }
+ }
+
@MJI
public int getReturnType____Ljava_lang_Class_2 (MJIEnv env, int objRef){
MethodInfo mi = getMethodInfo(env, objRef);
--- /dev/null
+package gov.nasa.jpf.test.vm.basic;
+
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.reflect.Method;
+import java.util.Arrays;
+import java.util.Objects;
+
+import org.junit.Test;
+
+import gov.nasa.jpf.test.vm.basic.AnnotationToStringTest.EnumConsts;
+import gov.nasa.jpf.util.test.TestJPF;
+
+public class AnnotationDefaultValueReflectionTest extends TestJPF {
+ public class NotAnAnnotation {
+ public void method() {
+
+ }
+ }
+
+ @Test
+ public void testNoDefaultValue() throws NoSuchMethodException, SecurityException {
+ Method m = NotAnAnnotation.class.getDeclaredMethod("method");
+ assertNull(m.getDefaultValue());
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A0 {
+ boolean f1() default true;
+
+ boolean f2();
+ }
+
+ @Test
+ public void testBooleanAttributeDefaultValue() throws NoSuchMethodException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = A0.class;
+ Method f1 = klass.getDeclaredMethod("f1");
+ Method f2 = klass.getDeclaredMethod("f2");
+ assertNull(f2.getDefaultValue());
+ boolean expected = true;
+ Object defaultValue = f1.getDefaultValue();
+ assertTrue(expected == (boolean) defaultValue);
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A1 {
+ boolean[] f1() default { true, false };
+
+ boolean[] f2();
+ }
+
+ @Test
+ public void testBooleanArrayAttributeDefaultValue() throws NoSuchMethodException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = A1.class;
+ Method f1 = klass.getDeclaredMethod("f1");
+ Method f2 = klass.getDeclaredMethod("f2");
+ assertNull(f2.getDefaultValue());
+ boolean[] expected = { true, false };
+ Object defaultValue = f1.getDefaultValue();
+ assertTrue(Arrays.equals(expected, (boolean[]) defaultValue));
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A2 {
+ byte f1() default 2;
+
+ byte f2();
+ }
+
+ @Test
+ public void testByteAttributeDefaultValue() throws NoSuchMethodException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = A2.class;
+ Method f1 = klass.getDeclaredMethod("f1");
+ Method f2 = klass.getDeclaredMethod("f2");
+ assertNull(f2.getDefaultValue());
+ byte expected = 2;
+ Object defaultValue = f1.getDefaultValue();
+ assertTrue(expected == (byte) defaultValue);
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A3 {
+ byte[] f1() default { 2, 3 };
+
+ byte[] f2();
+ }
+
+ @Test
+ public void testByteArrayAttributeDefaultValue() throws NoSuchMethodException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = A3.class;
+ Method f1 = klass.getDeclaredMethod("f1");
+ Method f2 = klass.getDeclaredMethod("f2");
+ assertNull(f2.getDefaultValue());
+ byte[] expected = { 2, 3 };
+ Object defaultValue = f1.getDefaultValue();
+ assertTrue(Arrays.equals(expected, (byte[]) defaultValue));
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A4 {
+ char f1() default 'a';
+
+ char f2();
+ }
+
+ @Test
+ public void testCharAttributeDefaultValue() throws NoSuchMethodException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = A4.class;
+ Method f1 = klass.getDeclaredMethod("f1");
+ Method f2 = klass.getDeclaredMethod("f2");
+ assertNull(f2.getDefaultValue());
+ char expected = 'a';
+ Object defaultValue = f1.getDefaultValue();
+ assertTrue(expected == (char) defaultValue);
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A5 {
+ char[] f1() default { 'a', 'b' };
+
+ char[] f2();
+ }
+
+ @Test
+ public void testCharArrayAttributeDefaultValue() throws NoSuchMethodException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = A5.class;
+ Method f1 = klass.getDeclaredMethod("f1");
+ Method f2 = klass.getDeclaredMethod("f2");
+ assertNull(f2.getDefaultValue());
+ char[] expected = { 'a', 'b' };
+ Object defaultValue = f1.getDefaultValue();
+ assertTrue(Arrays.equals(expected, (char[]) defaultValue));
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A6 {
+ short f1() default 0;
+
+ short f2();
+ }
+
+ @Test
+ public void testShortAttributeDefaultValue() throws NoSuchMethodException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = A6.class;
+ Method f1 = klass.getDeclaredMethod("f1");
+ Method f2 = klass.getDeclaredMethod("f2");
+ assertNull(f2.getDefaultValue());
+ short expected = 0;
+ Object defaultValue = f1.getDefaultValue();
+ assertTrue(expected == (short) defaultValue);
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A7 {
+ short[] f1() default { 0, 1 };
+
+ short[] f2();
+ }
+
+ @Test
+ public void testShortArrayAttributeDefaultValue() throws NoSuchMethodException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = A7.class;
+ Method f1 = klass.getDeclaredMethod("f1");
+ Method f2 = klass.getDeclaredMethod("f2");
+ assertNull(f2.getDefaultValue());
+ short[] expected = { 0, 1 };
+ Object defaultValue = f1.getDefaultValue();
+ assertTrue(Arrays.equals(expected, (short[]) defaultValue));
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A8 {
+ int f1() default 4;
+
+ int f2();
+ }
+
+ @Test
+ public void testIntAttributeDefaultValue() throws NoSuchMethodException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = A8.class;
+ Method f1 = klass.getDeclaredMethod("f1");
+ Method f2 = klass.getDeclaredMethod("f2");
+ assertNull(f2.getDefaultValue());
+ int expected = 4;
+ Object defaultValue = f1.getDefaultValue();
+ assertTrue(expected == (int) defaultValue);
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A9 {
+ int[] f1() default { 4, 5 };
+
+ int[] f2();
+ }
+
+ @Test
+ public void testIntArrayAttributeDefaultValue() throws NoSuchMethodException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = A9.class;
+ Method f1 = klass.getDeclaredMethod("f1");
+ Method f2 = klass.getDeclaredMethod("f2");
+ assertNull(f2.getDefaultValue());
+ int[] expected = { 4, 5 };
+ Object defaultValue = f1.getDefaultValue();
+ assertTrue(Arrays.equals(expected, (int[]) defaultValue));
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A10 {
+ long f1() default 9L;
+
+ long f2();
+ }
+
+ @Test
+ public void testLongAttributeDefaultValue() throws NoSuchMethodException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = A10.class;
+ Method f1 = klass.getDeclaredMethod("f1");
+ Method f2 = klass.getDeclaredMethod("f2");
+ assertNull(f2.getDefaultValue());
+ long expected = 9L;
+ Object defaultValue = f1.getDefaultValue();
+ assertTrue(expected == (long) defaultValue);
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A11 {
+ long[] f1() default { 9L, 10L };
+
+ long[] f2();
+ }
+
+ @Test
+ public void testLongArrayAttributeDefaultValue() throws NoSuchMethodException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = A11.class;
+ Method f1 = klass.getDeclaredMethod("f1");
+ Method f2 = klass.getDeclaredMethod("f2");
+ assertNull(f2.getDefaultValue());
+ long[] expected = { 9L, 10L };
+ Object defaultValue = f1.getDefaultValue();
+ assertTrue(Arrays.equals(expected, (long[]) defaultValue));
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A12 {
+ float f1() default 0.5f;
+
+ float f2();
+ }
+
+ @Test
+ public void testFloatAttributeDefaultValue() throws NoSuchMethodException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = A12.class;
+ Method f1 = klass.getDeclaredMethod("f1");
+ Method f2 = klass.getDeclaredMethod("f2");
+ assertNull(f2.getDefaultValue());
+ float expected = 0.5f;
+ Object defaultValue = f1.getDefaultValue();
+ assertTrue(expected == (float) defaultValue);
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A13 {
+ float[] f1() default { 0.5f, 2.0f };
+
+ float[] f2();
+ }
+
+ @Test
+ public void testFloatArrayAttributeDefaultValue() throws NoSuchMethodException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = A13.class;
+ Method f1 = klass.getDeclaredMethod("f1");
+ Method f2 = klass.getDeclaredMethod("f2");
+ assertNull(f2.getDefaultValue());
+ float[] expected = { 0.5f, 2.0f };
+ Object defaultValue = f1.getDefaultValue();
+ assertTrue(Arrays.equals(expected, (float[]) defaultValue));
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A14 {
+ double f1() default 2.0;
+
+ double f2();
+ }
+
+ @Test
+ public void testDoubleAttributeDefaultValue() throws NoSuchMethodException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = A14.class;
+ Method f1 = klass.getDeclaredMethod("f1");
+ Method f2 = klass.getDeclaredMethod("f2");
+ assertNull(f2.getDefaultValue());
+ double expected = 2.0;
+ Object defaultValue = f1.getDefaultValue();
+ assertTrue(expected == (double) defaultValue);
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A15 {
+ double[] f1() default { 2.0, 3.5 };
+
+ double[] f2();
+ }
+
+ @Test
+ public void testDoubleArrayAttributeDefaultValue() throws NoSuchMethodException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = A15.class;
+ Method f1 = klass.getDeclaredMethod("f1");
+ Method f2 = klass.getDeclaredMethod("f2");
+ assertNull(f2.getDefaultValue());
+ double[] expected = { 2.0, 3.5 };
+ Object defaultValue = f1.getDefaultValue();
+ assertTrue(Arrays.equals(expected, (double[]) defaultValue));
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A16 {
+ String f1() default "Hello";
+
+ String f2();
+ }
+
+ @Test
+ public void testStringAttributeDefaultValue() throws NoSuchMethodException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = A16.class;
+ Method f1 = klass.getDeclaredMethod("f1");
+ Method f2 = klass.getDeclaredMethod("f2");
+ assertNull(f2.getDefaultValue());
+ String expected = "Hello";
+ Object defaultValue = f1.getDefaultValue();
+ assertEquals(expected, (String) defaultValue);
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A17 {
+ String[] f1() default { "Hello", "World" };
+
+ String[] f2();
+ }
+
+ @Test
+ public void testStringArrayAttributeDefaultValue() throws NoSuchMethodException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = A17.class;
+ Method f1 = klass.getDeclaredMethod("f1");
+ Method f2 = klass.getDeclaredMethod("f2");
+ assertNull(f2.getDefaultValue());
+ String[] expected = { "Hello", "World" };
+ Object defaultValue = f1.getDefaultValue();
+ assertTrue(Arrays.equals(expected, (String[]) defaultValue));
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A18 {
+ Class<?> f1() default String.class;
+
+ Class<?> f2();
+ }
+
+ @Test
+ public void testClassAttributeDefaultValue() throws NoSuchMethodException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = A18.class;
+ Method f1 = klass.getDeclaredMethod("f1");
+ Method f2 = klass.getDeclaredMethod("f2");
+ assertNull(f2.getDefaultValue());
+ Class<?> expected = String.class;
+ Object defaultValue = f1.getDefaultValue();
+ assertEquals(expected, (Class<?>) defaultValue);
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A19 {
+ Class<?>[] f1() default { String.class, Integer.class };
+
+ Class<?>[] f2();
+ }
+
+ @Test
+ public void testClassArrayAttributeDefaultValue() throws NoSuchMethodException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = A19.class;
+ Method f1 = klass.getDeclaredMethod("f1");
+ Method f2 = klass.getDeclaredMethod("f2");
+ assertNull(f2.getDefaultValue());
+ Class<?>[] expected = { String.class, Integer.class };
+ Object defaultValue = f1.getDefaultValue();
+ assertTrue(Arrays.equals(expected, (Class<?>[]) defaultValue));
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A20 {
+ EnumConsts f1() default EnumConsts.FIRST;
+
+ EnumConsts f2();
+ }
+
+ @Test
+ public void testEnumConstsAttributeDefaultValue() throws NoSuchMethodException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = A20.class;
+ Method f1 = klass.getDeclaredMethod("f1");
+ Method f2 = klass.getDeclaredMethod("f2");
+ assertNull(f2.getDefaultValue());
+ EnumConsts expected = EnumConsts.FIRST;
+ Object defaultValue = f1.getDefaultValue();
+ assertEquals(expected, (EnumConsts) defaultValue);
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A21 {
+ EnumConsts[] f1() default { EnumConsts.FIRST, EnumConsts.SECOND };
+
+ EnumConsts[] f2();
+ }
+
+ @Test
+ public void testEnumConstsArrayAttributeDefaultValue() throws NoSuchMethodException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = A21.class;
+ Method f1 = klass.getDeclaredMethod("f1");
+ Method f2 = klass.getDeclaredMethod("f2");
+ assertNull(f2.getDefaultValue());
+ EnumConsts[] expected = { EnumConsts.FIRST, EnumConsts.SECOND };
+ Object defaultValue = f1.getDefaultValue();
+ assertTrue(Arrays.equals(expected, (EnumConsts[]) defaultValue));
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface Nested {
+ A0 f1() default @A0(f2 = true);
+ A16 f2();
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A22 {
+ Nested f1() default @Nested(f2 = @A16(f1 = "Hello", f2 = "World"));
+ }
+
+ @Nested(f2 = @A16(f1 = "Hello", f2 = "World"))
+ public static class Holder {
+ }
+
+ @Test
+ public void testAnnotationAttributeDefaultValue() throws NoSuchMethodException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = A22.class;
+ Method f1 = klass.getDeclaredMethod("f1");
+ Nested expected = Holder.class.getAnnotation(Nested.class);
+ Object defaultValue = f1.getDefaultValue();
+ assertEquals(expected, defaultValue);
+ }
+ }
+}
--- /dev/null
+package gov.nasa.jpf.test.vm.basic;
+
+import org.junit.Test;
+
+import gov.nasa.jpf.test.vm.basic.AnnotationToStringTest.*;
+import gov.nasa.jpf.util.test.TestJPF;
+
+public class AnnotationHashCodeEqualsTest extends TestJPF {
+ public class C0 {
+ @A0(f1 = true, f2 = false)
+ public int f1;
+
+ @A0(f1 = true, f2 = false)
+ public int f2;
+
+ @A0(f1 = false, f2 = true)
+ public int f3;
+ }
+
+ @Test
+ public void testBooleanAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C0.class;
+ A0 a = klass.getDeclaredField("f1").getAnnotation(A0.class);
+ A0 b = klass.getDeclaredField("f2").getAnnotation(A0.class);
+ A0 c = klass.getDeclaredField("f3").getAnnotation(A0.class);
+ assertEquals(a, b);
+ assertEquals(a.hashCode(), b.hashCode());
+ assertFalse(c.equals(b));
+ assertFalse(c.equals(a));
+ }
+ }
+
+ public class C1 {
+ @A1(f1 = { true, false }, f2 = { false, true })
+ public int f1;
+
+ @A1(f1 = { true, false }, f2 = { false, true })
+ public int f2;
+
+ @A1(f1 = { false, true }, f2 = { true, false })
+ public int f3;
+ }
+
+ @Test
+ public void testBooleanArrayAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C1.class;
+ A1 a = klass.getDeclaredField("f1").getAnnotation(A1.class);
+ A1 b = klass.getDeclaredField("f2").getAnnotation(A1.class);
+ A1 c = klass.getDeclaredField("f3").getAnnotation(A1.class);
+ assertEquals(a, b);
+ assertEquals(a.hashCode(), b.hashCode());
+ assertFalse(c.equals(b));
+ assertFalse(c.equals(a));
+ }
+ }
+
+ public class C2 {
+ @A2(f1 = 2, f2 = 3)
+ public int f1;
+
+ @A2(f1 = 2, f2 = 3)
+ public int f2;
+
+ @A2(f1 = 3, f2 = 2)
+ public int f3;
+ }
+
+ @Test
+ public void testByteAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C2.class;
+ A2 a = klass.getDeclaredField("f1").getAnnotation(A2.class);
+ A2 b = klass.getDeclaredField("f2").getAnnotation(A2.class);
+ A2 c = klass.getDeclaredField("f3").getAnnotation(A2.class);
+ assertEquals(a, b);
+ assertEquals(a.hashCode(), b.hashCode());
+ assertFalse(c.equals(b));
+ assertFalse(c.equals(a));
+ }
+ }
+
+ public class C3 {
+ @A3(f1 = { 2, 3 }, f2 = { 3, 2 })
+ public int f1;
+
+ @A3(f1 = { 2, 3 }, f2 = { 3, 2 })
+ public int f2;
+
+ @A3(f1 = { 3, 2 }, f2 = { 2, 3 })
+ public int f3;
+ }
+
+ @Test
+ public void testByteArrayAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C3.class;
+ A3 a = klass.getDeclaredField("f1").getAnnotation(A3.class);
+ A3 b = klass.getDeclaredField("f2").getAnnotation(A3.class);
+ A3 c = klass.getDeclaredField("f3").getAnnotation(A3.class);
+ assertEquals(a, b);
+ assertEquals(a.hashCode(), b.hashCode());
+ assertFalse(c.equals(b));
+ assertFalse(c.equals(a));
+ }
+ }
+
+ public class C4 {
+ @A4(f1 = 'a', f2 = 'b')
+ public int f1;
+
+ @A4(f1 = 'a', f2 = 'b')
+ public int f2;
+
+ @A4(f1 = 'b', f2 = 'a')
+ public int f3;
+ }
+
+ @Test
+ public void testCharAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C4.class;
+ A4 a = klass.getDeclaredField("f1").getAnnotation(A4.class);
+ A4 b = klass.getDeclaredField("f2").getAnnotation(A4.class);
+ A4 c = klass.getDeclaredField("f3").getAnnotation(A4.class);
+ assertEquals(a, b);
+ assertEquals(a.hashCode(), b.hashCode());
+ assertFalse(c.equals(b));
+ assertFalse(c.equals(a));
+ }
+ }
+
+ public class C5 {
+ @A5(f1 = { 'a', 'b' }, f2 = { 'b', 'a' })
+ public int f1;
+
+ @A5(f1 = { 'a', 'b' }, f2 = { 'b', 'a' })
+ public int f2;
+
+ @A5(f1 = { 'b', 'a' }, f2 = { 'a', 'b' })
+ public int f3;
+ }
+
+ @Test
+ public void testCharArrayAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C5.class;
+ A5 a = klass.getDeclaredField("f1").getAnnotation(A5.class);
+ A5 b = klass.getDeclaredField("f2").getAnnotation(A5.class);
+ A5 c = klass.getDeclaredField("f3").getAnnotation(A5.class);
+ assertEquals(a, b);
+ assertEquals(a.hashCode(), b.hashCode());
+ assertFalse(c.equals(b));
+ assertFalse(c.equals(a));
+ }
+ }
+
+ public class C6 {
+ @A6(f1 = 0, f2 = 1)
+ public int f1;
+
+ @A6(f1 = 0, f2 = 1)
+ public int f2;
+
+ @A6(f1 = 1, f2 = 0)
+ public int f3;
+ }
+
+ @Test
+ public void testShortAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C6.class;
+ A6 a = klass.getDeclaredField("f1").getAnnotation(A6.class);
+ A6 b = klass.getDeclaredField("f2").getAnnotation(A6.class);
+ A6 c = klass.getDeclaredField("f3").getAnnotation(A6.class);
+ assertEquals(a, b);
+ assertEquals(a.hashCode(), b.hashCode());
+ assertFalse(c.equals(b));
+ assertFalse(c.equals(a));
+ }
+ }
+
+ public class C7 {
+ @A7(f1 = { 0, 1 }, f2 = { 1, 0 })
+ public int f1;
+
+ @A7(f1 = { 0, 1 }, f2 = { 1, 0 })
+ public int f2;
+
+ @A7(f1 = { 1, 0 }, f2 = { 0, 1 })
+ public int f3;
+ }
+
+ @Test
+ public void testShortArrayAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C7.class;
+ A7 a = klass.getDeclaredField("f1").getAnnotation(A7.class);
+ A7 b = klass.getDeclaredField("f2").getAnnotation(A7.class);
+ A7 c = klass.getDeclaredField("f3").getAnnotation(A7.class);
+ assertEquals(a, b);
+ assertEquals(a.hashCode(), b.hashCode());
+ assertFalse(c.equals(b));
+ assertFalse(c.equals(a));
+ }
+ }
+
+ public class C8 {
+ @A8(f1 = 4, f2 = 5)
+ public int f1;
+
+ @A8(f1 = 4, f2 = 5)
+ public int f2;
+
+ @A8(f1 = 5, f2 = 4)
+ public int f3;
+ }
+
+ @Test
+ public void testIntAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C8.class;
+ A8 a = klass.getDeclaredField("f1").getAnnotation(A8.class);
+ A8 b = klass.getDeclaredField("f2").getAnnotation(A8.class);
+ A8 c = klass.getDeclaredField("f3").getAnnotation(A8.class);
+ assertEquals(a, b);
+ assertEquals(a.hashCode(), b.hashCode());
+ assertFalse(c.equals(b));
+ assertFalse(c.equals(a));
+ }
+ }
+
+ public class C9 {
+ @A9(f1 = { 4, 5 }, f2 = { 5, 4 })
+ public int f1;
+
+ @A9(f1 = { 4, 5 }, f2 = { 5, 4 })
+ public int f2;
+
+ @A9(f1 = { 5, 4 }, f2 = { 4, 5 })
+ public int f3;
+ }
+
+ @Test
+ public void testIntArrayAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C9.class;
+ A9 a = klass.getDeclaredField("f1").getAnnotation(A9.class);
+ A9 b = klass.getDeclaredField("f2").getAnnotation(A9.class);
+ A9 c = klass.getDeclaredField("f3").getAnnotation(A9.class);
+ assertEquals(a, b);
+ assertEquals(a.hashCode(), b.hashCode());
+ assertFalse(c.equals(b));
+ assertFalse(c.equals(a));
+ }
+ }
+
+ public class C10 {
+ @A10(f1 = 9L, f2 = 10L)
+ public int f1;
+
+ @A10(f1 = 9L, f2 = 10L)
+ public int f2;
+
+ @A10(f1 = 10L, f2 = 9L)
+ public int f3;
+ }
+
+ @Test
+ public void testLongAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C10.class;
+ A10 a = klass.getDeclaredField("f1").getAnnotation(A10.class);
+ A10 b = klass.getDeclaredField("f2").getAnnotation(A10.class);
+ A10 c = klass.getDeclaredField("f3").getAnnotation(A10.class);
+ assertEquals(a, b);
+ assertEquals(a.hashCode(), b.hashCode());
+ assertFalse(c.equals(b));
+ assertFalse(c.equals(a));
+ }
+ }
+
+ public class C11 {
+ @A11(f1 = { 9L, 10L }, f2 = { 10L, 9L })
+ public int f1;
+
+ @A11(f1 = { 9L, 10L }, f2 = { 10L, 9L })
+ public int f2;
+
+ @A11(f1 = { 10L, 9L }, f2 = { 9L, 10L })
+ public int f3;
+ }
+
+ @Test
+ public void testLongArrayAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C11.class;
+ A11 a = klass.getDeclaredField("f1").getAnnotation(A11.class);
+ A11 b = klass.getDeclaredField("f2").getAnnotation(A11.class);
+ A11 c = klass.getDeclaredField("f3").getAnnotation(A11.class);
+ assertEquals(a, b);
+ assertEquals(a.hashCode(), b.hashCode());
+ assertFalse(c.equals(b));
+ assertFalse(c.equals(a));
+ }
+ }
+
+ public class C12 {
+ @A12(f1 = 0.5f, f2 = 2.0f)
+ public int f1;
+
+ @A12(f1 = 0.5f, f2 = 2.0f)
+ public int f2;
+
+ @A12(f1 = 2.0f, f2 = 0.5f)
+ public int f3;
+ }
+
+ @Test
+ public void testFloatAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C12.class;
+ A12 a = klass.getDeclaredField("f1").getAnnotation(A12.class);
+ A12 b = klass.getDeclaredField("f2").getAnnotation(A12.class);
+ A12 c = klass.getDeclaredField("f3").getAnnotation(A12.class);
+ assertEquals(a, b);
+ assertEquals(a.hashCode(), b.hashCode());
+ assertFalse(c.equals(b));
+ assertFalse(c.equals(a));
+ }
+ }
+
+ public class C13 {
+ @A13(f1 = { 0.5f, 2.0f }, f2 = { 2.0f, 0.5f })
+ public int f1;
+
+ @A13(f1 = { 0.5f, 2.0f }, f2 = { 2.0f, 0.5f })
+ public int f2;
+
+ @A13(f1 = { 2.0f, 0.5f }, f2 = { 0.5f, 2.0f })
+ public int f3;
+ }
+
+ @Test
+ public void testFloatArrayAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C13.class;
+ A13 a = klass.getDeclaredField("f1").getAnnotation(A13.class);
+ A13 b = klass.getDeclaredField("f2").getAnnotation(A13.class);
+ A13 c = klass.getDeclaredField("f3").getAnnotation(A13.class);
+ assertEquals(a, b);
+ assertEquals(a.hashCode(), b.hashCode());
+ assertFalse(c.equals(b));
+ assertFalse(c.equals(a));
+ }
+ }
+
+ public class C14 {
+ @A14(f1 = 2.0, f2 = 3.5)
+ public int f1;
+
+ @A14(f1 = 2.0, f2 = 3.5)
+ public int f2;
+
+ @A14(f1 = 3.5, f2 = 2.0)
+ public int f3;
+ }
+
+ @Test
+ public void testDoubleAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C14.class;
+ A14 a = klass.getDeclaredField("f1").getAnnotation(A14.class);
+ A14 b = klass.getDeclaredField("f2").getAnnotation(A14.class);
+ A14 c = klass.getDeclaredField("f3").getAnnotation(A14.class);
+ assertEquals(a, b);
+ assertEquals(a.hashCode(), b.hashCode());
+ assertFalse(c.equals(b));
+ assertFalse(c.equals(a));
+ }
+ }
+
+ public class C15 {
+ @A15(f1 = { 2.0, 3.5 }, f2 = { 3.5, 2.0 })
+ public int f1;
+
+ @A15(f1 = { 2.0, 3.5 }, f2 = { 3.5, 2.0 })
+ public int f2;
+
+ @A15(f1 = { 3.5, 2.0 }, f2 = { 2.0, 3.5 })
+ public int f3;
+ }
+
+ @Test
+ public void testDoubleArrayAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C15.class;
+ A15 a = klass.getDeclaredField("f1").getAnnotation(A15.class);
+ A15 b = klass.getDeclaredField("f2").getAnnotation(A15.class);
+ A15 c = klass.getDeclaredField("f3").getAnnotation(A15.class);
+ assertEquals(a, b);
+ assertEquals(a.hashCode(), b.hashCode());
+ assertFalse(c.equals(b));
+ assertFalse(c.equals(a));
+ }
+ }
+
+ public class C16 {
+ @A16(f1 = "Hello", f2 = "World")
+ public int f1;
+
+ @A16(f1 = "Hello", f2 = "World")
+ public int f2;
+
+ @A16(f1 = "World", f2 = "Hello")
+ public int f3;
+ }
+
+ @Test
+ public void testStringAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C16.class;
+ A16 a = klass.getDeclaredField("f1").getAnnotation(A16.class);
+ A16 b = klass.getDeclaredField("f2").getAnnotation(A16.class);
+ A16 c = klass.getDeclaredField("f3").getAnnotation(A16.class);
+ assertEquals(a, b);
+ assertEquals(a.hashCode(), b.hashCode());
+ assertFalse(c.equals(b));
+ assertFalse(c.equals(a));
+ }
+ }
+
+ public class C17 {
+ @A17(f1 = { "Hello", "World" }, f2 = { "World", "Hello" })
+ public int f1;
+
+ @A17(f1 = { "Hello", "World" }, f2 = { "World", "Hello" })
+ public int f2;
+
+ @A17(f1 = { "World", "Hello" }, f2 = { "Hello", "World" })
+ public int f3;
+ }
+
+ @Test
+ public void testStringArrayAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C17.class;
+ A17 a = klass.getDeclaredField("f1").getAnnotation(A17.class);
+ A17 b = klass.getDeclaredField("f2").getAnnotation(A17.class);
+ A17 c = klass.getDeclaredField("f3").getAnnotation(A17.class);
+ assertEquals(a, b);
+ assertEquals(a.hashCode(), b.hashCode());
+ assertFalse(c.equals(b));
+ assertFalse(c.equals(a));
+ }
+ }
+
+ public class C18 {
+ @A18(f1 = String.class, f2 = Integer.class)
+ public int f1;
+
+ @A18(f1 = String.class, f2 = Integer.class)
+ public int f2;
+
+ @A18(f1 = Integer.class, f2 = String.class)
+ public int f3;
+ }
+
+ @Test
+ public void testClassAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C18.class;
+ A18 a = klass.getDeclaredField("f1").getAnnotation(A18.class);
+ A18 b = klass.getDeclaredField("f2").getAnnotation(A18.class);
+ A18 c = klass.getDeclaredField("f3").getAnnotation(A18.class);
+ assertEquals(a, b);
+ assertEquals(a.hashCode(), b.hashCode());
+ assertFalse(c.equals(b));
+ assertFalse(c.equals(a));
+ }
+ }
+
+ public class C19 {
+ @A19(f1 = { String.class, Integer.class }, f2 = { Integer.class, String.class })
+ public int f1;
+
+ @A19(f1 = { String.class, Integer.class }, f2 = { Integer.class, String.class })
+ public int f2;
+
+ @A19(f1 = { Integer.class, String.class }, f2 = { String.class, Integer.class })
+ public int f3;
+ }
+
+ @Test
+ public void testClassArrayAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C19.class;
+ A19 a = klass.getDeclaredField("f1").getAnnotation(A19.class);
+ A19 b = klass.getDeclaredField("f2").getAnnotation(A19.class);
+ A19 c = klass.getDeclaredField("f3").getAnnotation(A19.class);
+ assertEquals(a, b);
+ assertEquals(a.hashCode(), b.hashCode());
+ assertFalse(c.equals(b));
+ assertFalse(c.equals(a));
+ }
+ }
+
+ public class C20 {
+ @A20(f1 = EnumConsts.FIRST, f2 = EnumConsts.SECOND)
+ public int f1;
+
+ @A20(f1 = EnumConsts.FIRST, f2 = EnumConsts.SECOND)
+ public int f2;
+
+ @A20(f1 = EnumConsts.SECOND, f2 = EnumConsts.FIRST)
+ public int f3;
+ }
+
+ @Test
+ public void testEnumConstsAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C20.class;
+ A20 a = klass.getDeclaredField("f1").getAnnotation(A20.class);
+ A20 b = klass.getDeclaredField("f2").getAnnotation(A20.class);
+ A20 c = klass.getDeclaredField("f3").getAnnotation(A20.class);
+ assertEquals(a, b);
+ assertEquals(a.hashCode(), b.hashCode());
+ assertFalse(c.equals(b));
+ assertFalse(c.equals(a));
+ }
+ }
+
+ public class C21 {
+ @A21(f1 = { EnumConsts.FIRST, EnumConsts.SECOND }, f2 = { EnumConsts.SECOND, EnumConsts.FIRST })
+ public int f1;
+
+ @A21(f1 = { EnumConsts.FIRST, EnumConsts.SECOND }, f2 = { EnumConsts.SECOND, EnumConsts.FIRST })
+ public int f2;
+
+ @A21(f1 = { EnumConsts.SECOND, EnumConsts.FIRST }, f2 = { EnumConsts.FIRST, EnumConsts.SECOND })
+ public int f3;
+ }
+
+ @Test
+ public void testEnumConstsArrayAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C21.class;
+ A21 a = klass.getDeclaredField("f1").getAnnotation(A21.class);
+ A21 b = klass.getDeclaredField("f2").getAnnotation(A21.class);
+ A21 c = klass.getDeclaredField("f3").getAnnotation(A21.class);
+ assertEquals(a, b);
+ assertEquals(a.hashCode(), b.hashCode());
+ assertFalse(c.equals(b));
+ assertFalse(c.equals(a));
+ }
+ }
+
+ public class C22 {
+ @A22(f1 = @Nested1(fields = @A16(f1 = "Hello", f2 = "World")), f2 = @Nested2(fields = @A1(f1 = false, f2 = false)))
+ public int f1;
+
+ @A22(f1 = @Nested1(fields = @A16(f1 = "Hello", f2 = "World")), f2 = @Nested2(fields = @A1(f1 = false, f2 = false)))
+ public int f2;
+
+ @A22(f1 = @Nested1(fields = @A16(f1 = "Hola", f2 = "Mundo")), f2 = @Nested2(fields = @A1(f1 = true, f2 = true)))
+ public int f3;
+ }
+
+ @Test
+ public void testAnnotationAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C22.class;
+ A22 a = klass.getDeclaredField("f1").getAnnotation(A22.class);
+ A22 b = klass.getDeclaredField("f2").getAnnotation(A22.class);
+ A22 c = klass.getDeclaredField("f3").getAnnotation(A22.class);
+ assertEquals(a, b);
+ assertEquals(a.hashCode(), b.hashCode());
+ assertFalse(c.equals(b));
+ assertFalse(c.equals(a));
+ }
+ }
+
+ public class C23 {
+ @A23(f1 = {
+ @Nested1(fields = @A16(f1 = "Hello", f2 = "World")),
+ @Nested1(fields = @A16(f1 = "Bonjour", f2 = "Monde"))
+ }, f2 = {
+ @Nested2(fields = @A1(f1 = false, f2 = false)),
+ @Nested2(fields = @A1(f1 = true, f2 = true))
+ })
+ public int f1;
+
+ @A23(f1 = {
+ @Nested1(fields = @A16(f1 = "Hello", f2 = "World")),
+ @Nested1(fields = @A16(f1 = "Bonjour", f2 = "Monde"))
+ }, f2 = {
+ @Nested2(fields = @A1(f1 = false, f2 = false)),
+ @Nested2(fields = @A1(f1 = true, f2 = true))
+ })
+ public int f2;
+
+ @A23(f1 = {
+ @Nested1(fields = @A16(f1 = "Hola", f2 = "Mundo")),
+ @Nested1(fields = @A16(f1 = "Bonjour", f2 = "Monde"))
+ }, f2 = {
+ @Nested2(fields = @A1(f1 = false, f2 = true)),
+ @Nested2(fields = @A1(f1 = true, f2 = false))
+ }) public int f3;
+ }
+
+ @Test
+ public void testAnnotationArrayAttributeHashCodeEquals() throws NoSuchFieldException, SecurityException {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C23.class;
+ A23 a = klass.getDeclaredField("f1").getAnnotation(A23.class);
+ A23 b = klass.getDeclaredField("f2").getAnnotation(A23.class);
+ A23 c = klass.getDeclaredField("f3").getAnnotation(A23.class);
+ assertEquals(a, b);
+ assertEquals(a.hashCode(), b.hashCode());
+ assertFalse(c.equals(b));
+ assertFalse(c.equals(a));
+ }
+ }
+
+}
--- /dev/null
+package gov.nasa.jpf.test.vm.basic;
+
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+
+import org.junit.Test;
+
+import gov.nasa.jpf.util.test.TestJPF;
+
+public class AnnotationToStringTest extends TestJPF {
+ private static final String TTFF_NESTED = "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$Nested2("
+ + "fields=@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A1(f1=[false,false],f2=[true,true]))";
+ private static final String HELLO_WORLD_NESTED = "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$Nested1("
+ + "fields=@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A16(f1=Hello,f2=World))";
+
+
+ public static enum EnumConsts {
+ FIRST, SECOND
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A0 {
+ boolean f1();
+
+ boolean f2();
+ }
+
+ @A0(f1 = true, f2 = false)
+ public class C0 {
+ }
+
+ @Test
+ public void testBooleanAttributeToString() {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C0.class;
+ A0 a = klass.getAnnotation(A0.class);
+ System.out.println(a.toString());
+ assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A0(f1=true,f2=false)");
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A1 {
+ boolean[] f1();
+
+ boolean[] f2();
+ }
+
+ @A1(f1 = { true, false }, f2 = { false, true })
+ public class C1 {
+ }
+
+ @Test
+ public void testBooleanArrayAttributeToString() {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C1.class;
+ A1 a = klass.getAnnotation(A1.class);
+ assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A1(f1=[true,false],f2=[false,true])");
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A2 {
+ byte f1();
+
+ byte f2();
+ }
+
+ @A2(f1 = 0, f2 = 1)
+ public class C2 {
+ }
+
+ @Test
+ public void testByteAttributeToString() {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C2.class;
+ A2 a = klass.getAnnotation(A2.class);
+ assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A2(f1=0,f2=1)");
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A3 {
+ byte[] f1();
+
+ byte[] f2();
+ }
+
+ @A3(f1 = { 0, 1 }, f2 = { 1, 0 })
+ public class C3 {
+ }
+
+ @Test
+ public void testByteArrayAttributeToString() {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C3.class;
+ A3 a = klass.getAnnotation(A3.class);
+ assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A3(f1=[0,1],f2=[1,0])");
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A4 {
+ char f1();
+
+ char f2();
+ }
+
+ @A4(f1 = 'a', f2 = 'b')
+ public class C4 {
+ }
+
+ @Test
+ public void testCharAttributeToString() {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C4.class;
+ A4 a = klass.getAnnotation(A4.class);
+ assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A4(f1=a,f2=b)");
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A5 {
+ char[] f1();
+
+ char[] f2();
+ }
+
+ @A5(f1 = { 'a', 'b' }, f2 = { 'b', 'a' })
+ public class C5 {
+ }
+
+ @Test
+ public void testCharArrayAttributeToString() {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C5.class;
+ A5 a = klass.getAnnotation(A5.class);
+ assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A5(f1=[a,b],f2=[b,a])");
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A6 {
+ short f1();
+
+ short f2();
+ }
+
+ @A6(f1 = 0, f2 = 1)
+ public class C6 {
+ }
+
+ @Test
+ public void testShortAttributeToString() {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C6.class;
+ A6 a = klass.getAnnotation(A6.class);
+ assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A6(f1=0,f2=1)");
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A7 {
+ short[] f1();
+
+ short[] f2();
+ }
+
+ @A7(f1 = { 0, 1 }, f2 = { 1, 0 })
+ public class C7 {
+ }
+
+ @Test
+ public void testShortArrayAttributeToString() {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C7.class;
+ A7 a = klass.getAnnotation(A7.class);
+ assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A7(f1=[0,1],f2=[1,0])");
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A8 {
+ int f1();
+
+ int f2();
+ }
+
+ @A8(f1 = 0, f2 = 1)
+ public class C8 {
+ }
+
+ @Test
+ public void testIntAttributeToString() {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C8.class;
+ A8 a = klass.getAnnotation(A8.class);
+ assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A8(f1=0,f2=1)");
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A9 {
+ int[] f1();
+
+ int[] f2();
+ }
+
+ @A9(f1 = { 0, 1 }, f2 = { 1, 0 })
+ public class C9 {
+ }
+
+ @Test
+ public void testIntArrayAttributeToString() {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C9.class;
+ A9 a = klass.getAnnotation(A9.class);
+ assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A9(f1=[0,1],f2=[1,0])");
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A10 {
+ long f1();
+
+ long f2();
+ }
+
+ @A10(f1 = 1L, f2 = 10L)
+ public class C10 {
+ }
+
+ @Test
+ public void testLongAttributeToString() {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C10.class;
+ A10 a = klass.getAnnotation(A10.class);
+ assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A10(f1=1,f2=10)");
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A11 {
+ long[] f1();
+
+ long[] f2();
+ }
+
+ @A11(f1 = { 1L, 10L }, f2 = { 10L, 1L })
+ public class C11 {
+ }
+
+ @Test
+ public void testLongArrayAttributeToString() {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C11.class;
+ A11 a = klass.getAnnotation(A11.class);
+ assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A11(f1=[1,10],f2=[10,1])");
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A12 {
+ float f1();
+
+ float f2();
+ }
+
+ @A12(f1 = 0.5f, f2 = 2.0f)
+ public class C12 {
+ }
+
+ @Test
+ public void testFloatAttributeToString() {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C12.class;
+ A12 a = klass.getAnnotation(A12.class);
+ assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A12(f1=0.5,f2=2.0)");
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A13 {
+ float[] f1();
+
+ float[] f2();
+ }
+
+ @A13(f1 = { 0.5f, 2.0f }, f2 = { 2.0f, 0.5f })
+ public class C13 {
+ }
+
+ @Test
+ public void testFloatArrayAttributeToString() {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C13.class;
+ A13 a = klass.getAnnotation(A13.class);
+ assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A13(f1=[0.5,2.0],f2=[2.0,0.5])");
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A14 {
+ double f1();
+
+ double f2();
+ }
+
+ @A14(f1 = 2.0, f2 = 3.5)
+ public class C14 {
+ }
+
+ @Test
+ public void testDoubleAttributeToString() {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C14.class;
+ A14 a = klass.getAnnotation(A14.class);
+ assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A14(f1=2.0,f2=3.5)");
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A15 {
+ double[] f1();
+
+ double[] f2();
+ }
+
+ @A15(f1 = { 2.0, 3.5 }, f2 = { 3.5, 2.0 })
+ public class C15 {
+ }
+
+ @Test
+ public void testDoubleArrayAttributeToString() {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C15.class;
+ A15 a = klass.getAnnotation(A15.class);
+ assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A15(f1=[2.0,3.5],f2=[3.5,2.0])");
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A16 {
+ String f1();
+
+ String f2();
+ }
+
+ @A16(f1 = "Hello", f2 = "World")
+ public class C16 {
+ }
+
+ @Test
+ public void testStringAttributeToString() {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C16.class;
+ A16 a = klass.getAnnotation(A16.class);
+ assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A16(f1=Hello,f2=World)");
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A17 {
+ String[] f1();
+
+ String[] f2();
+ }
+
+ @A17(f1 = { "Hello", "World" }, f2 = { "World", "Hello" })
+ public class C17 {
+ }
+
+ @Test
+ public void testStringArrayAttributeToString() {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C17.class;
+ A17 a = klass.getAnnotation(A17.class);
+ System.out.println(a.toString());
+ assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A17(f1=[Hello,World],f2=[World,Hello])");
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A18 {
+ Class<?> f1();
+
+ Class<?> f2();
+ }
+
+ @A18(f1 = String.class, f2 = Integer.class)
+ public class C18 {
+ }
+
+ @Test
+ public void testClassAttributeToString() {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C18.class;
+ A18 a = klass.getAnnotation(A18.class);
+ System.out.println(a.toString());
+ assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A18(f1=class java.lang.String,f2=class java.lang.Integer)");
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A19 {
+ Class<?>[] f1();
+
+ Class<?>[] f2();
+ }
+
+ @A19(f1 = { String.class, Integer.class }, f2 = { Integer.class, String.class })
+ public class C19 {
+ }
+
+ @Test
+ public void testClassArrayAttributeToString() {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C19.class;
+ A19 a = klass.getAnnotation(A19.class);
+ assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A19(f1=[class java.lang.String,class java.lang.Integer],"
+ + "f2=[class java.lang.Integer,class java.lang.String])");
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A20 {
+ EnumConsts f1();
+
+ EnumConsts f2();
+ }
+
+ @A20(f1 = EnumConsts.FIRST, f2 = EnumConsts.SECOND)
+ public class C20 {
+ }
+
+ @Test
+ public void testEnumConstsAttributeToString() {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C20.class;
+ A20 a = klass.getAnnotation(A20.class);
+ assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A20(f1=gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$EnumConsts.FIRST,"
+ + "f2=gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$EnumConsts.SECOND)");
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A21 {
+ EnumConsts[] f1();
+
+ EnumConsts[] f2();
+ }
+
+ @A21(f1 = { EnumConsts.FIRST, EnumConsts.SECOND }, f2 = { EnumConsts.SECOND, EnumConsts.FIRST })
+ public class C21 {
+ }
+
+ @Test
+ public void testEnumConstsArrayAttributeToString() {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C21.class;
+ A21 a = klass.getAnnotation(A21.class);
+ assertEquals(a.toString(), "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A21("
+ + "f1=[gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$EnumConsts.FIRST,gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$EnumConsts.SECOND],"
+ + "f2=[gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$EnumConsts.SECOND,gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$EnumConsts.FIRST])");
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface Nested1 {
+ A16 fields();
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface Nested2 {
+ A1 fields();
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A22 {
+ Nested1 f1();
+ Nested2 f2();
+ }
+
+ @A22(f1 = @Nested1(fields = @A16(f1 = "Hello", f2 = "World")), f2 = @Nested2(fields = @A1(f1 = {false, false}, f2 = {true, true})))
+ public class C22 {
+
+ }
+
+ @Test
+ public void testAnnotationAttributeToString() {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C22.class;
+ A22 a = klass.getAnnotation(A22.class);
+ String toString = "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A22(f1=" + HELLO_WORLD_NESTED + ",f2=" + TTFF_NESTED + ")";
+ assertEquals(a.toString(), a.toString(), toString);
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface A23 {
+ Nested1[] f1();
+ Nested2[] f2();
+ }
+
+ @A23(f1 = {
+ @Nested1(fields = @A16(f1 = "Hello", f2 = "World")), @Nested1(fields = @A16(f1 = "Hola", f2 = "Mundo"))
+ }, f2 = {
+ @Nested2(fields = @A1(f1 = {false, false}, f2 = {true, true})), @Nested2(fields = @A1(f1 = {true,true}, f2 = {false,false}))
+ })
+ public class C23 {
+
+ }
+
+ @Test
+ public void testAnnotationArrayAttributeToString() {
+ if(verifyNoPropertyViolation()) {
+ Class<?> klass = C23.class;
+ A23 a = klass.getAnnotation(A23.class);
+ String holaMundo = HELLO_WORLD_NESTED.replace("Hello", "Hola").replace("World", "Mundo");
+ String trueTrueString = TTFF_NESTED.replaceAll("false", "TMP").replaceAll("true", "false").replaceAll("TMP", "true");
+ String toString = "@gov.nasa.jpf.test.vm.basic.AnnotationToStringTest$A23(f1=[" + HELLO_WORLD_NESTED + "," + holaMundo + "],"
+ + "f2=[" + TTFF_NESTED + "," + trueTrueString + "])";
+ assertEquals(a.toString(), toString);
+ }
+ }
+}
--- /dev/null
+package gov.nasa.jpf.test.vm.basic;
+
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+
+import org.junit.Test;
+
+import gov.nasa.jpf.jvm.JVMSystemClassLoaderInfo;
+import gov.nasa.jpf.util.test.TestJPF;
+import gov.nasa.jpf.vm.AnnotationInfo;
+import gov.nasa.jpf.vm.ClassInfoException;
+import gov.nasa.jpf.vm.VM;
+
+public class MissingAnnotationClassTest extends TestJPF {
+ public static class SkippingSystemClassLoader extends JVMSystemClassLoaderInfo {
+ public SkippingSystemClassLoader(VM vm, int appId) {
+ super(vm, appId);
+ }
+
+ @Override
+ public AnnotationInfo getResolvedAnnotationInfo(String typeName) throws ClassInfoException {
+ if(typeName.equals("gov.nasa.jpf.test.vm.basic.MissingAnnotationClassTest$Nullable")) {
+ throw new ClassInfoException("class not found: " + typeName, this, "java.lang.ClassNotFoundException", typeName);
+ }
+ return super.getResolvedAnnotationInfo(typeName);
+ }
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface Nullable {
+ }
+
+ @Retention(RetentionPolicy.RUNTIME)
+ public @interface Present {
+ }
+
+ @Present
+ @Nullable
+ public static class AnnotatedClass {
+
+ }
+
+ @Test
+ public void testMissingAnnotationOk() {
+ if(verifyNoPropertyViolation("+vm.classloader.class=gov.nasa.jpf.test.vm.basic.MissingAnnotationClassTest$SkippingSystemClassLoader")) {
+ assertEquals(1, AnnotatedClass.class.getAnnotations().length);
+ }
+ }
+}
projects / jpf-core.git / commitdiff