Add ability to mark methods as ignored (not loaded)

Author: NathanJPhillips

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -118,7 +118,15 @@ class java_bytecode_convert_classt:public messaget
   // see definition below for more info
   static void add_array_types(symbol_tablet &symbol_table);
 
-  static bool is_overlay_method(const methodt &method);
+  static bool is_overlay_method(const methodt &method)
+  {
+    return method.has_annotation(ID_overlay_method);
+  }
+
+  static bool is_ignored_method(const methodt &method)
+  {
+    return method.has_annotation(ID_ignored_method);
+  }
 
   bool check_field_exists(
     const fieldt &field,
@@ -455,6 +463,8 @@ void java_bytecode_convert_classt::convert(
   {
     for(const methodt &method : overlay_class.get().methods)
     {
+      if(is_ignored_method(method))
+        continue;
       const irep_idt method_identifier =
         qualified_classname + "." + id2string(method.name)
           + ":" + method.descriptor;
@@ -496,6 +506,8 @@ void java_bytecode_convert_classt::convert(
   }
   for(const methodt &method : c.methods)
   {
+    if(is_ignored_method(method))
+      continue;
     const irep_idt method_identifier=
       qualified_classname + "." + id2string(method.name)
         + ":" + method.descriptor;
@@ -877,13 +889,6 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
   }
 }
 
-bool java_bytecode_convert_classt::is_overlay_method(const methodt &method)
-{
-  return java_bytecode_parse_treet::find_annotation(
-           method.annotations, ID_overlay_method)
-    .has_value();
-}
-
 bool java_bytecode_convert_class(
   const java_class_loadert::parse_tree_with_overlayst &parse_trees,
   symbol_tablet &symbol_table,

jbmc/src/java_bytecode/java_bytecode_parse_tree.h

@@ -84,6 +84,11 @@ class java_bytecode_parse_treet
       is_private(false), is_static(false), is_final(false)
     {
     }
+
+    bool has_annotation(const irep_idt &annotation_id) const
+    {
+      return find_annotation(annotations, annotation_id).has_value();
+    }
   };
 
   class methodt:public membert

src/util/irep_ids.def

@@ -664,6 +664,7 @@ IREP_ID_TWO(overflow_shl, overflow-shl)
 IREP_ID_TWO(C_no_initialization_required, #no_initialization_required)
 IREP_ID_TWO(overlay_class, java::com.diffblue.OverlayClassImplementation)
 IREP_ID_TWO(overlay_method, java::com.diffblue.OverlayMethodImplementation)
+IREP_ID_TWO(ignored_method, java::com.diffblue.IgnoredMethodImplementation)
 IREP_ID_ONE(is_annotation)
 IREP_ID_TWO(C_annotations, #annotations)
 IREP_ID_ONE(final)