Rename _start to __CPROVER_start

regression/cbmc/graphml_witness1/test.desc

@@ -46,29 +46,29 @@ main.c
   <graph edgedefault="directed">
     <data key="sourcecodelang">C</data>
     <node id="sink"/>
-    <node id="33.22">
+    <node id="[0-9\.]*">
       <data key="entry">true</data>
     </node>
-    <edge source="33.22" target="4.29">
+    <edge source="[0-9\.]*" target="[0-9\.]*">
       <data key="originfile">main.c</data>
       <data key="startline">21</data>
     </edge>
-    <node id="4.29"/>
-    <edge source="4.29" target="29.31">
+    <node id="[0-9\.]*"/>
+    <edge source="[0-9\.]*" target="[0-9\.]*">
       <data key="originfile">main.c</data>
       <data key="startline">29</data>
       <data key="assumption.scope">main</data>
     </edge>
-    <node id="29.31"/>
-    <edge source="29.31" target="5.33">
+    <node id="[0-9\.]*"/>
+    <edge source="[0-9\.]*" target="[0-9\.]*">
       <data key="originfile">main.c</data>
       <data key="startline">15</data>
       <data key="assumption.scope">remove_one</data>
     </edge>
-    <node id="5.33">
+    <node id="[0-9\.]*">
       <data key="violation">true</data>
     </node>
-    <edge source="5.33" target="sink">
+    <edge source="[0-9\.]*" target="sink">
       <data key="originfile">main.c</data>
       <data key="startline">31</data>
     </edge>

src/cbmc/symex_coverage.cpp

@@ -276,7 +276,7 @@ void symex_coveraget::compute_overall_coverage(
   forall_goto_functions(gf_it, goto_functions)
   {
     if(!gf_it->second.body_available() ||
-       gf_it->first==ID__start ||
+       gf_it->first==goto_functions.entry_point() ||
        gf_it->first==CPROVER_PREFIX "initialize")
       continue;
 

src/cegis/invariant/fitness/concrete_fitness_source_provider.cpp

@@ -69,9 +69,15 @@ bool contains(const std::string &haystack, const std::string &needle)
   return std::string::npos != haystack.find(needle);
 }
 
-bool handle_start(std::string &source, const std::string &line)
+bool handle_start(
+  const goto_functionst &gf,
+  std::string &source,
+  const std::string &line)
 {
-  if ("void _start(void)" != line) return false;
+  std::ostringstream start_sig;
+  start_sig << "void " << gf.entry_point() << "(void)";
+  if(start_sig.str()!=line)
+    return false;
   source+="int main(const int argc, const char * const argv[])\n";
   return true;
 }
@@ -212,17 +218,24 @@ bool handle_internals(const std::string &line)
       || "static signed int assert#return_value;" == line;
 }
 
-void post_process(std::string &source, std::stringstream &ss)
+void post_process(
+  const goto_functionst &gf,
+  std::string &source,
+  std::stringstream &ss)
 {
   bool deserialise_initialised=false;
   bool ce_initialised=false;
   for (std::string line; std::getline(ss, line);)
   {
-    if (handle_start(source, line) || handle_return_value(line)
-        || handle_ce_loop(line, ss) || handle_internals(line)
-        || handle_programs(source, deserialise_initialised, line)
-        || handle_x0(source, line) || handle_ce(source, ce_initialised, line)
-        || handle_second_instr_struct(source, line)) continue;
+    if(handle_start(gf, source, line) ||
+       handle_return_value(line) ||
+       handle_ce_loop(line, ss) ||
+       handle_internals(line) ||
+       handle_programs(source, deserialise_initialised, line) ||
+       handle_x0(source, line) ||
+       handle_ce(source, ce_initialised, line) ||
+       handle_second_instr_struct(source, line))
+      continue;
     replace_ce_index(line);
     replace_assume(line);
     fix_cprover_names(line);
@@ -254,7 +267,7 @@ std::string &post_process_fitness_source(std::string &result,
   add_first_prog_offset(result, num_ce_vars);
   add_assume_implementation(result);
   add_danger_execute(result, num_vars, num_consts, max_prog_size, exec);
-  post_process(result, ss);
+  post_process(gf, result, ss);
   transform_program_individual_main_to_lib(result, danger);
   return result;
 }

src/cegis/jsa/genetic/jsa_source_provider.cpp

@@ -26,7 +26,6 @@ jsa_source_providert::jsa_source_providert(jsa_symex_learnt &lcfg) :
 {
 }
 
-#define START_METHOD_PREFIX "void _start"
 #define RETURN_VALUE_ASSIGNMENT RETURN_VALUE_SUFFIX" ="
 #define JUMP_BUFFER "__CPROVER_jsa_jump_buffer"
 #define TEST_SIGNATURE "int " CEGIS_FITNESS_TEST_FUNC \
@@ -104,7 +103,9 @@ void add_main_body(std::string &result, const jsa_symex_learnt &lcfg)
   std::ostringstream oss;
   dump_c(entry_only, false, ns, oss);
   const std::string main_body(oss.str());
-  result+=main_body.substr(main_body.find(START_METHOD_PREFIX));
+  result+=
+    main_body.substr(
+      main_body.find(std::string("void ")+id2string(gf.entry_point())));
 }
 
 void fix_return_values(std::string &result)
@@ -138,9 +139,11 @@ void fix_return_values(std::string &result)
   substitute(result, "\n  return 0;", "");
 }
 
-void add_facade_function(std::string &result)
+void add_facade_function(const goto_functionst &gf, std::string &result)
 {
-  substitute(result, "void _start(void)", TEST_SIGNATURE);
+  std::ostringstream start_sig;
+  start_sig << "void " << gf.entry_point() << "(void)";
+  substitute(result, start_sig.str(), TEST_SIGNATURE);
   const std::string::size_type pos=result.find("  __CPROVER_initialize();");
   result.insert(pos, "  if (setjmp(" JUMP_BUFFER")) return EXIT_FAILURE;\n");
 }
@@ -249,7 +252,7 @@ const std::string &jsa_source_providert::operator ()()
   add_temp_clean(source, lcfg.get_symbol_table());
   add_main_body(source, lcfg);
   fix_return_values(source);
-  add_facade_function(source);
+  add_facade_function(lcfg.get_goto_functions(), source);
   insert_solution(source, lcfg);
   insert_counterexample(source);
   cleanup(source);

src/goto-instrument/cover.cpp

@@ -1391,7 +1391,7 @@ void instrument_cover_goals(
 {
   Forall_goto_functions(f_it, goto_functions)
   {
-    if(f_it->first==ID__start ||
+    if(f_it->first==goto_functions.entry_point() ||
        f_it->first=="__CPROVER_initialize")
       continue;
 

src/goto-programs/goto_functions_template.h

@@ -16,6 +16,7 @@ Date: June 2003
 
 #include <util/std_types.h>
 #include <util/symbol.h>
+#include <util/cprover_prefix.h>
 
 template <class bodyT>
 class goto_function_templatet
@@ -123,7 +124,7 @@ class goto_functions_templatet
   static inline irep_idt entry_point()
   {
     // do not confuse with C's "int main()"
-    return ID__start;
+    return CPROVER_PREFIX "_start";
   }
 
   void swap(goto_functions_templatet &other)

src/goto-programs/show_goto_functions_json.cpp

@@ -67,7 +67,7 @@ json_objectt show_goto_functions_jsont::convert(
     json_function["isBodyAvailable"]=
       jsont::json_boolean(function.body_available());
     bool is_internal=(has_prefix(id2string(function_name), CPROVER_PREFIX) ||
-                      function_name==ID__start);
+                      function_name==goto_functions.entry_point());
     json_function["isInternal"]=jsont::json_boolean(is_internal);
 
     if(function.body_available())

src/goto-programs/show_goto_functions_xml.cpp

@@ -80,7 +80,7 @@ xmlt show_goto_functions_xmlt::convert(
     xml_function.set_attribute_bool(
       "is_body_available", function.body_available());
     bool is_internal=(has_prefix(id2string(function_name), CPROVER_PREFIX) ||
-                      function_name==ID__start);
+                      function_name==goto_functions.entry_point());
     xml_function.set_attribute_bool("is_internal", is_internal);
 
     if(function.body_available())

src/util/irep_ids.txt

@@ -681,7 +681,6 @@ read
 write
 native
 final
-_start
 compound_literal
 custom_bv
 custom_unsignedbv