diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index cf4c4ccd83..654ecf44ce 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -425,7 +425,8 @@ static irep_idt get_method_identifier( void java_bytecode_convert_methodt::convert( const symbolt &class_symbol, - const methodt &m) + const methodt &m, + const optionalt &method_context) { // Construct the fully qualified method name // (e.g. "my.package.ClassName.myMethodName:(II)I") and query the symbol table @@ -605,8 +606,12 @@ void java_bytecode_convert_methodt::convert( if((!m.is_abstract) && (!m.is_native)) { code_blockt code(convert_parameter_annotations(m, method_type)); - code.append(convert_instructions(m)); - method_symbol.value = std::move(code); + // Do not convert if method is not in context + if(!method_context || (*method_context)(id2string(method_identifier))) + { + code.append(convert_instructions(m)); + method_symbol.value = std::move(code); + } } } @@ -3184,7 +3189,8 @@ void java_bytecode_convert_method( optionalt needed_lazy_methods, java_string_library_preprocesst &string_preprocess, const class_hierarchyt &class_hierarchy, - bool threading_support) + bool threading_support, + const optionalt &method_context) { java_bytecode_convert_methodt java_bytecode_convert_method( @@ -3197,7 +3203,7 @@ void java_bytecode_convert_method( class_hierarchy, threading_support); - java_bytecode_convert_method(class_symbol, method); + java_bytecode_convert_method(class_symbol, method, method_context); } /// Returns true iff method \p methodid from class \p classname is diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.h b/jbmc/src/java_bytecode/java_bytecode_convert_method.h index 7df5289262..9e7da32667 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.h +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.h @@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com #include class class_hierarchyt; +class prefix_filtert; void java_bytecode_initialize_parameter_names( symbolt &method_symbol, @@ -37,7 +38,8 @@ void java_bytecode_convert_method( optionalt needed_lazy_methods, java_string_library_preprocesst &string_preprocess, const class_hierarchyt &class_hierarchy, - bool threading_support); + bool threading_support, + const optionalt &method_context); void create_method_stub_symbol( const irep_idt &identifier, diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h b/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h index c10af8c214..d7f3104470 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h @@ -61,9 +61,12 @@ public: typedef methodt::local_variable_tablet local_variable_tablet; typedef methodt::local_variablet local_variablet; - void operator()(const symbolt &class_symbol, const methodt &method) + void operator()( + const symbolt &class_symbol, + const methodt &method, + const optionalt &method_context) { - convert(class_symbol, method); + convert(class_symbol, method, method_context); } typedef uint16_t method_offsett; @@ -290,7 +293,10 @@ protected: bool allow_merge = true); // conversion - void convert(const symbolt &class_symbol, const methodt &); + void convert( + const symbolt &class_symbol, + const methodt &, + const optionalt &method_context); code_blockt convert_parameter_annotations( const methodt &method, diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index 4a948e321a..253d670389 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -1173,12 +1173,6 @@ bool java_bytecode_languaget::convert_single_method( optionalt needed_lazy_methods, lazy_class_to_declared_symbols_mapt &class_to_declared_symbols) { - // Do not convert if method is not in context - if(method_context && !(*method_context)(id2string(function_id))) - { - return false; - } - const symbolt &symbol = symbol_table.lookup_ref(function_id); // Nothing to do if body is already loaded @@ -1312,7 +1306,8 @@ bool java_bytecode_languaget::convert_single_method( std::move(needed_lazy_methods), string_preprocess, class_hierarchy, - threading_support); + threading_support, + method_context); INVARIANT(declaring_class(symbol), "Method must have a declaring class."); return false; }