Assign parameter names to abstract functions that we're giving a stub…

… body
NathanJPhillips · Jul 31, 2018 · 264bc6f · 264bc6f
1 parent 4348968
commit 264bc6f
Show file tree

Hide file tree

Showing 3 changed files with 23 additions and 3 deletions.
diff --git a/cbmc/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/cbmc/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -85,7 +85,7 @@ class patternt
 /// \return Assigns parameter names (side-effects on `ftype`) to function stub
 ///   parameters, which are initially nameless as method conversion hasn't
 ///   happened. Also creates symbols in `symbol_table`.
-static void assign_parameter_names(
+void assign_parameter_names(
   code_typet &ftype,
   const irep_idt &name_prefix,
   symbol_table_baset &symbol_table)

diff --git a/cbmc/jbmc/src/java_bytecode/java_bytecode_convert_method.h b/cbmc/jbmc/src/java_bytecode/java_bytecode_convert_method.h
@@ -46,4 +46,9 @@ void java_bytecode_convert_method_lazy(
   symbol_tablet &symbol_table,
   message_handlert &);
 
+void assign_parameter_names(
+  code_typet &ftype,
+  const irep_idt &name_prefix,
+  symbol_table_baset &symbol_table);
+
 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_H
diff --git a/src/driver/sec_driver_parse_options.cpp b/src/driver/sec_driver_parse_options.cpp
@@ -32,6 +32,7 @@
 #include <analyses/local_may_alias.h>
 
 #include <java_bytecode/convert_java_nondet.h>
+#include <java_bytecode/java_bytecode_convert_method.h>
 #include <java_bytecode/remove_exceptions.h>
 #include <java_bytecode/remove_instanceof.h>
 #include <java_bytecode/remove_java_new.h>
@@ -659,17 +660,31 @@ bool sec_driver_parse_optionst::generate_function_body(
   goto_functiont &function,
   bool body_available)
 {
+  const symbolt *symbol = symbol_table.lookup(function_name);
+
   // Provide a simple stub implementation for any function we don't have a
   // bytecode implementation for:
   if(body_available || !can_generate_function_body(function_name))
   {
-    const symbolt *symbol = symbol_table.lookup(function_name);
     if(symbol == nullptr || !symbol->type.get_bool(ID_C_abstract))
       return false;
   }
 
-  if(symbol_table.lookup_ref(function_name).mode == ID_java)
+  if(symbol->mode == ID_java)
   {
+    code_typet code_type = to_code_type(symbol->type);
+
+    // Note this may invalidate pointer `symbol` by adding to the symtab, so:
+    symbol = nullptr;
+
+    if(
+      code_type.parameters().size() != 0 &&
+      code_type.parameters()[0].get_identifier().empty())
+    {
+      assign_parameter_names(code_type, function_name, symbol_table);
+      symbol_table.get_writeable_ref(function_name).type = code_type;
+    }
+
     java_generate_simple_method_stub(
       function_name,
       symbol_table,