fix Java member operator

Author: Daniel Kroening

src/java_bytecode/java_bytecode_typecheck_expr.cpp

@@ -162,38 +162,45 @@ Function: java_bytecode_typecheckt::typecheck_expr_symbol
 
 void java_bytecode_typecheckt::typecheck_expr_member(member_exprt &expr)
 {
-  // the member might be in a parent class
+  // The member might be in a parent class, which we resolve here.
   const irep_idt component_name=expr.get_component_name();
 
-  #if 0
   while(1)
   {
-    // TODO handle vtables
+    if(expr.struct_op().type().id()!=ID_struct)
+      break; // give up
+  
     const struct_typet &struct_type=
       to_struct_type(ns.follow(expr.struct_op().type()));
 
     if(struct_type.has_component(component_name))
       return; // done
 
     // look at parent
-    const struct_typet::componentst &components=struct_type.components();
+    const struct_typet::componentst &components=
+      struct_type.components();
 
     if(components.empty())
-    {
-      #if 0
-      warning().sourc_location=expr.source_location();
-      warning() << "failed to find field `"
-                << component_name << "` in class hierarchy" << eom;
-      #endif
-      return;
-    }
-    
+      break; // give up
+
     const struct_typet::componentt &c=components.front();
 
     member_exprt m(expr.struct_op(), c.get_name(), c.type());
     m.add_source_location()=expr.source_location();
 
     expr.struct_op()=m;
   }
+
+  #if 0
+  warning().source_location=expr.source_location();
+  warning() << "failed to find field `"
+            << component_name << "` in class hierarchy" << eom;
+  #else
+  warning_msg("failed to find field `"+
+              id2string(component_name)+"` in class hierarchy");
   #endif
+
+  // We replace by a non-det of same type
+  side_effect_expr_nondett nondet(expr.type());
+  expr.swap(nondet);
 }