diff --git a/regression/cbmc/graphml_witness1/test.desc b/regression/cbmc/graphml_witness1/test.desc index 9e7f5b42724..cb22eaba5d0 100644 --- a/regression/cbmc/graphml_witness1/test.desc +++ b/regression/cbmc/graphml_witness1/test.desc @@ -46,29 +46,29 @@ main.c C - + true - + main.c 21 - - + + main.c 29 main - - + + main.c 15 remove_one - + true - + main.c 31 diff --git a/src/cbmc/symex_coverage.cpp b/src/cbmc/symex_coverage.cpp index 69af02e9e9e..578eb26d913 100644 --- a/src/cbmc/symex_coverage.cpp +++ b/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; diff --git a/src/cegis/invariant/fitness/concrete_fitness_source_provider.cpp b/src/cegis/invariant/fitness/concrete_fitness_source_provider.cpp index 28e41138cb3..dbfa21257c5 100644 --- a/src/cegis/invariant/fitness/concrete_fitness_source_provider.cpp +++ b/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; } diff --git a/src/cegis/jsa/genetic/jsa_source_provider.cpp b/src/cegis/jsa/genetic/jsa_source_provider.cpp index 4984bfe1c9b..1182317f771 100644 --- a/src/cegis/jsa/genetic/jsa_source_provider.cpp +++ b/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); diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index ede599b6d8b..00a0bf86eff 100644 --- a/src/goto-instrument/cover.cpp +++ b/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; diff --git a/src/goto-programs/goto_functions_template.h b/src/goto-programs/goto_functions_template.h index 27757df4e87..7c427b4f72f 100644 --- a/src/goto-programs/goto_functions_template.h +++ b/src/goto-programs/goto_functions_template.h @@ -16,6 +16,7 @@ Date: June 2003 #include #include +#include template 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) diff --git a/src/goto-programs/show_goto_functions_json.cpp b/src/goto-programs/show_goto_functions_json.cpp index 1f61e30d2f6..47a19e0662a 100644 --- a/src/goto-programs/show_goto_functions_json.cpp +++ b/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()) diff --git a/src/goto-programs/show_goto_functions_xml.cpp b/src/goto-programs/show_goto_functions_xml.cpp index a5d1c9d5dd4..7ccdd71a4ff 100644 --- a/src/goto-programs/show_goto_functions_xml.cpp +++ b/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()) diff --git a/src/util/irep_ids.txt b/src/util/irep_ids.txt index 066a5f831cc..ab812d5f289 100644 --- a/src/util/irep_ids.txt +++ b/src/util/irep_ids.txt @@ -681,7 +681,6 @@ read write native final -_start compound_literal custom_bv custom_unsignedbv