| Code with Finding: |
class InstConstraintVisitor {
/**
* Ensures the specific preconditions of the said instruction.
*/
@Override
public void visitPUTSTATIC(PUTSTATIC o){
try {
String field_name = o.getFieldName(cpg);
JavaClass jc = Repository.lookupClass(getObjectType(o).getClassName());
Field[] fields = jc.getFields();
Field f = null;
for (Field field : fields) {
if (field.getName().equals(field_name)){
Type f_type = Type.getType(field.getSignature());
Type o_type = o.getType(cpg);
/* TODO: Check if assignment compatibility is sufficient.
* What does Sun do?
*/
if (f_type.equals(o_type)){
f = field;
break;
}
}
}
if (f == null){
throw new AssertionViolatedException("Field '" + field_name + "' not found in " + jc.getClassName());
}
Type value = stack().peek();
Type t = Type.getType(f.getSignature());
Type shouldbe = t;
if (shouldbe == Type.BOOLEAN ||
shouldbe == Type.BYTE ||
shouldbe == Type.CHAR ||
shouldbe == Type.SHORT){
shouldbe = Type.INT;
}
if (t instanceof ReferenceType){
ReferenceType rvalue = null;
if (value instanceof ReferenceType){
rvalue = (ReferenceType) value;
referenceTypeIsInitialized(o, rvalue);
}
else{
constraintViolated(o, "The stack top type '"+value+"' is not of a reference type as expected.");
}
// TODO: This can possibly only be checked using Staerk-et-al's "set-of-object types", not
// using "wider cast object types" created during verification.
// Comment it out if you encounter problems. See also the analogon at visitPUTFIELD.
if (!(rvalue.isAssignmentCompatibleWith(shouldbe))){
constraintViolated(o, "The stack top type '"+value+"' is not assignment compatible with '"+shouldbe+"'.");
}
}
else{
if (shouldbe != value){
constraintViolated(o, "The stack top type '"+value+"' is not of type '"+shouldbe+"' as expected.");
}
}
// TODO: Interface fields may be assigned to only once. (Hard to implement in
// JustIce's execution model). This may only happen in <clinit>, see Pass 3a.
} catch (ClassNotFoundException e) {
// FIXME: maybe not the best way to handle this
throw new AssertionViolatedException("Missing class: " + e, e);
}
}
}
|
