Amend condition for when stub method body should be made

There are three types of method symbols that we expect here:
1) symbols for regular methods, i.e. the bytecode of the method is
available and the method is in the supplied context
2) symbols for opaque methods, i.e. the bytecode of the method is not
available
3) symbols for excluded methods, i.e. the bytecode of the method is
available but the method is not in the supplied context
The previous check was correct for 1) and 2): we do not want to create
stub bodies ("return nondet") for regular methods but we do want to
create them for opaque methods.
The new check makes sure that stub bodies are also created for excluded
methods (3). Previously the value of those symbols was just left as nil,
meaning the (type of the) return value of the method was not constrained
in any way.

Author: antlechner

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -104,7 +104,7 @@ void parse_java_language_options(const cmdlinet &cmd, optionst &options)
   }
 }
 
-static prefix_filtert get_context(const optionst &options)
+prefix_filtert get_context(const optionst &options)
 {
   std::vector<std::string> context_include;
   std::vector<std::string> context_exclude;

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -304,4 +304,6 @@ std::unique_ptr<languaget> new_java_bytecode_language();
 
 void parse_java_language_options(const cmdlinet &cmd, optionst &options);
 
+prefix_filtert get_context(const optionst &options);
+
 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -690,6 +690,8 @@ int jbmc_parse_optionst::get_goto_program(
   std::unique_ptr<abstract_goto_modelt> &goto_model_ptr,
   const optionst &options)
 {
+  if(options.is_set("context-include") || options.is_set("context-exclude"))
+    method_context = get_context(options);
   lazy_goto_modelt lazy_goto_model =
     lazy_goto_modelt::from_handler_object(*this, options, ui_message_handler);
   lazy_goto_model.initialize(cmdline.args, options);
@@ -1009,7 +1011,9 @@ bool jbmc_parse_optionst::generate_function_body(
   // Provide a simple stub implementation for any function we don't have a
   // bytecode implementation for:
 
-  if(body_available)
+  if(
+    body_available &&
+    (!method_context || (*method_context)(id2string(function_name))))
     return false;
 
   if(!can_generate_function_body(function_name))

jbmc/src/jbmc/jbmc_parse_options.h

@@ -133,6 +133,11 @@ class jbmc_parse_optionst : public parse_options_baset
     const optionst &);
   bool show_loaded_functions(const abstract_goto_modelt &goto_model);
   bool show_loaded_symbols(const abstract_goto_modelt &goto_model);
+
+  /// See java_bytecode_languaget::method_context.
+  /// The two fields are initialized in exactly the same way.
+  /// TODO Refactor this so it only needs to be computed once, in one place.
+  optionalt<prefix_filtert> method_context;
 };
 
 #endif // CPROVER_JBMC_JBMC_PARSE_OPTIONS_H