Merge pull request #6784 from tautschnig/bugfixes/reachable-functions

Set base_name member for __CPROVER_start

Author: tautschnig

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -767,6 +767,7 @@ bool generate_java_start_function(
   symbolt new_symbol;
 
   new_symbol.name=goto_functionst::entry_point();
+  new_symbol.base_name = goto_functionst::entry_point();
   new_symbol.type = java_method_typet({}, java_void_type());
   new_symbol.value.swap(init_code);
   new_symbol.mode=ID_java;

regression/goto-analyzer/reachable-functions-basic-json/test.desc

@@ -10,3 +10,4 @@ CORE
 --
 "last line":[[:space:]]*$
 ^warning: ignoring
+"function": ""

regression/goto-analyzer/reachable-functions-basic-text/test.desc

@@ -9,3 +9,4 @@ unreachable.c not_obviously_dead 25 31$
 ^SIGNAL=0$
 --
 ^warning: ignoring
+^ 35$

src/ansi-c/ansi_c_entry_point.cpp

@@ -544,6 +544,7 @@ bool generate_ansi_c_start_function(
   symbolt new_symbol;
 
   new_symbol.name=goto_functionst::entry_point();
+  new_symbol.base_name = goto_functionst::entry_point();
   new_symbol.type = code_typet({}, void_type());
   new_symbol.value.swap(init_code);
   new_symbol.mode=symbol.mode;

src/jsil/jsil_entry_point.cpp

@@ -152,6 +152,7 @@ bool jsil_entry_point(
   symbolt new_symbol;
 
   new_symbol.name=goto_functionst::entry_point();
+  new_symbol.base_name = goto_functionst::entry_point();
   new_symbol.type = code_typet({}, empty_typet());
   new_symbol.value.swap(init_code);
 

src/statement-list/statement_list_entry_point.cpp

@@ -180,6 +180,7 @@ bool generate_statement_list_start_function(
   // Add the start symbol.
   symbolt start_symbol;
   start_symbol.name = goto_functionst::entry_point();
+  start_symbol.base_name = goto_functionst::entry_point();
   start_symbol.type = code_typet({}, empty_typet{});
   start_symbol.value.swap(start_function_body);
   start_symbol.mode = main.mode;

unit/analyses/ai/ai.cpp

@@ -233,6 +233,7 @@ SCENARIO(
 
   symbolt start;
   start.name = goto_functionst::entry_point();
+  start.base_name = goto_functionst::entry_point();
   start.mode = ID_C;
   start.type = code_typet({}, empty_typet());
   start.value = make_void_call(f.symbol_expr());