Rename _start to __CPROVER_start
While identifiers starting with _ are reserved according to the C standard, people nevertheless use them. Using __CPROVER_start will make collisions less likely. Includes cleanup such that there is exactly one point where this name is spelled out.
This commit is contained in:
parent
b56a33909c
commit
9c68c079fe
|
@ -49,7 +49,7 @@ main.c
|
||||||
<node id="[0-9\.]*">
|
<node id="[0-9\.]*">
|
||||||
<data key="entry">true</data>
|
<data key="entry">true</data>
|
||||||
</node>
|
</node>
|
||||||
<edge source="33.22" target="4.29">
|
<edge source="[0-9\.]*" target="[0-9\.]*">
|
||||||
<data key="originfile">main.c</data>
|
<data key="originfile">main.c</data>
|
||||||
<data key="startline">21</data>
|
<data key="startline">21</data>
|
||||||
</edge>
|
</edge>
|
||||||
|
|
|
@ -276,7 +276,7 @@ void symex_coveraget::compute_overall_coverage(
|
||||||
forall_goto_functions(gf_it, goto_functions)
|
forall_goto_functions(gf_it, goto_functions)
|
||||||
{
|
{
|
||||||
if(!gf_it->second.body_available() ||
|
if(!gf_it->second.body_available() ||
|
||||||
gf_it->first==ID__start ||
|
gf_it->first==goto_functions.entry_point() ||
|
||||||
gf_it->first==CPROVER_PREFIX "initialize")
|
gf_it->first==CPROVER_PREFIX "initialize")
|
||||||
continue;
|
continue;
|
||||||
|
|
||||||
|
|
|
@ -69,9 +69,15 @@ bool contains(const std::string &haystack, const std::string &needle)
|
||||||
return std::string::npos != haystack.find(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";
|
source+="int main(const int argc, const char * const argv[])\n";
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
|
@ -212,17 +218,24 @@ bool handle_internals(const std::string &line)
|
||||||
|| "static signed int assert#return_value;" == 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 deserialise_initialised=false;
|
||||||
bool ce_initialised=false;
|
bool ce_initialised=false;
|
||||||
for (std::string line; std::getline(ss, line);)
|
for (std::string line; std::getline(ss, line);)
|
||||||
{
|
{
|
||||||
if (handle_start(source, line) || handle_return_value(line)
|
if(handle_start(gf, source, line) ||
|
||||||
|| handle_ce_loop(line, ss) || handle_internals(line)
|
handle_return_value(line) ||
|
||||||
|| handle_programs(source, deserialise_initialised, line)
|
handle_ce_loop(line, ss) ||
|
||||||
|| handle_x0(source, line) || handle_ce(source, ce_initialised, line)
|
handle_internals(line) ||
|
||||||
|| handle_second_instr_struct(source, line)) continue;
|
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_ce_index(line);
|
||||||
replace_assume(line);
|
replace_assume(line);
|
||||||
fix_cprover_names(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_first_prog_offset(result, num_ce_vars);
|
||||||
add_assume_implementation(result);
|
add_assume_implementation(result);
|
||||||
add_danger_execute(result, num_vars, num_consts, max_prog_size, exec);
|
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);
|
transform_program_individual_main_to_lib(result, danger);
|
||||||
return result;
|
return result;
|
||||||
}
|
}
|
||||||
|
|
|
@ -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 RETURN_VALUE_ASSIGNMENT RETURN_VALUE_SUFFIX" ="
|
||||||
#define JUMP_BUFFER "__CPROVER_jsa_jump_buffer"
|
#define JUMP_BUFFER "__CPROVER_jsa_jump_buffer"
|
||||||
#define TEST_SIGNATURE "int " CEGIS_FITNESS_TEST_FUNC \
|
#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;
|
std::ostringstream oss;
|
||||||
dump_c(entry_only, false, ns, oss);
|
dump_c(entry_only, false, ns, oss);
|
||||||
const std::string main_body(oss.str());
|
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)
|
void fix_return_values(std::string &result)
|
||||||
|
@ -138,9 +139,11 @@ void fix_return_values(std::string &result)
|
||||||
substitute(result, "\n return 0;", "");
|
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();");
|
const std::string::size_type pos=result.find(" __CPROVER_initialize();");
|
||||||
result.insert(pos, " if (setjmp(" JUMP_BUFFER")) return EXIT_FAILURE;\n");
|
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_temp_clean(source, lcfg.get_symbol_table());
|
||||||
add_main_body(source, lcfg);
|
add_main_body(source, lcfg);
|
||||||
fix_return_values(source);
|
fix_return_values(source);
|
||||||
add_facade_function(source);
|
add_facade_function(lcfg.get_goto_functions(), source);
|
||||||
insert_solution(source, lcfg);
|
insert_solution(source, lcfg);
|
||||||
insert_counterexample(source);
|
insert_counterexample(source);
|
||||||
cleanup(source);
|
cleanup(source);
|
||||||
|
|
|
@ -1391,7 +1391,7 @@ void instrument_cover_goals(
|
||||||
{
|
{
|
||||||
Forall_goto_functions(f_it, goto_functions)
|
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")
|
f_it->first=="__CPROVER_initialize")
|
||||||
continue;
|
continue;
|
||||||
|
|
||||||
|
|
|
@ -16,6 +16,7 @@ Date: June 2003
|
||||||
|
|
||||||
#include <util/std_types.h>
|
#include <util/std_types.h>
|
||||||
#include <util/symbol.h>
|
#include <util/symbol.h>
|
||||||
|
#include <util/cprover_prefix.h>
|
||||||
|
|
||||||
template <class bodyT>
|
template <class bodyT>
|
||||||
class goto_function_templatet
|
class goto_function_templatet
|
||||||
|
@ -123,7 +124,7 @@ public:
|
||||||
static inline irep_idt entry_point()
|
static inline irep_idt entry_point()
|
||||||
{
|
{
|
||||||
// do not confuse with C's "int main()"
|
// do not confuse with C's "int main()"
|
||||||
return ID__start;
|
return CPROVER_PREFIX "_start";
|
||||||
}
|
}
|
||||||
|
|
||||||
void swap(goto_functions_templatet &other)
|
void swap(goto_functions_templatet &other)
|
||||||
|
|
|
@ -67,7 +67,7 @@ json_objectt show_goto_functions_jsont::convert(
|
||||||
json_function["isBodyAvailable"]=
|
json_function["isBodyAvailable"]=
|
||||||
jsont::json_boolean(function.body_available());
|
jsont::json_boolean(function.body_available());
|
||||||
bool is_internal=(has_prefix(id2string(function_name), CPROVER_PREFIX) ||
|
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);
|
json_function["isInternal"]=jsont::json_boolean(is_internal);
|
||||||
|
|
||||||
if(function.body_available())
|
if(function.body_available())
|
||||||
|
|
|
@ -80,7 +80,7 @@ xmlt show_goto_functions_xmlt::convert(
|
||||||
xml_function.set_attribute_bool(
|
xml_function.set_attribute_bool(
|
||||||
"is_body_available", function.body_available());
|
"is_body_available", function.body_available());
|
||||||
bool is_internal=(has_prefix(id2string(function_name), CPROVER_PREFIX) ||
|
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);
|
xml_function.set_attribute_bool("is_internal", is_internal);
|
||||||
|
|
||||||
if(function.body_available())
|
if(function.body_available())
|
||||||
|
|
|
@ -681,7 +681,6 @@ read
|
||||||
write
|
write
|
||||||
native
|
native
|
||||||
final
|
final
|
||||||
_start
|
|
||||||
compound_literal
|
compound_literal
|
||||||
custom_bv
|
custom_bv
|
||||||
custom_unsignedbv
|
custom_unsignedbv
|
||||||
|
|
Loading…
Reference in New Issue