Skip to content

Commit d351a5d

Browse files
tautschnigtautschnig
committed
Use a single global INITIALIZE_FUNCTION macro instead of __CPROVER_initialize
1 parent 9c03ca3 commit d351a5d

22 files changed

+69
-46
lines changed

‎src/ansi-c/ansi_c_entry_point.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ Author: Daniel Kroening, [email protected]
2323
#include <util/symbol.h>
2424

2525
#include <goto-programs/goto_functions.h>
26+
2627
#include <linking/static_lifetime_init.h>
2728

2829
#include "c_nondet_symbol_factory.h"
@@ -217,7 +218,7 @@ bool generate_ansi_c_start_function(
217218
if(init_it==symbol_table.symbols.end())
218219
{
219220
messaget message(message_handler);
220-
message.error() << "failed to find " CPROVER_PREFIX "initialize symbol"
221+
message.error() << "failed to find " INITIALIZE_FUNCTION " symbol"
221222
<< messaget::eom;
222223
return true;
223224
}

‎src/ansi-c/ansi_c_internal_additions.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,8 @@ Author: Daniel Kroening, [email protected]
1010

1111
#include <util/config.h>
1212

13+
#include <linking/static_lifetime_init.h>
14+
1315
const char gcc_builtin_headers_types[]=
1416
"# 1 \"gcc_builtin_headers_types.h\"\n"
1517
#include "gcc_builtin_headers_types.inc"
@@ -172,7 +174,7 @@ void ansi_c_internal_additions(std::string &code)
172174
"\n"
173175
// This function needs to be declared, or otherwise can't be called
174176
// by the entry-point construction.
175-
"void __CPROVER_initialize(void);\n"
177+
"void " INITIALIZE_FUNCTION "(void);\n"
176178
"\n";
177179

178180
// GCC junk stuff, also for CLANG and ARM

‎src/cbmc/bmc.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,8 @@ Author: Daniel Kroening, [email protected]
4242
#include <goto-symex/memory_model_tso.h>
4343
#include <goto-symex/memory_model_pso.h>
4444

45+
#include <linking/static_lifetime_init.h>
46+
4547
#include "cbmc_solvers.h"
4648
#include "counterexample_beautification.h"
4749
#include "fault_localization.h"
@@ -338,7 +340,7 @@ void bmct::setup()
338340

339341
{
340342
const symbolt *init_symbol;
341-
if(!ns.lookup(CPROVER_PREFIX "initialize", init_symbol))
343+
if(!ns.lookup(INITIALIZE_FUNCTION, init_symbol))
342344
symex.language_mode=init_symbol->mode;
343345
}
344346

‎src/cbmc/symex_coverage.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,8 @@ Date: March 2016
2929
#include <goto-programs/goto_functions.h>
3030
#include <goto-programs/remove_returns.h>
3131

32+
#include <linking/static_lifetime_init.h>
33+
3234
class coverage_recordt
3335
{
3436
public:
@@ -313,7 +315,7 @@ void symex_coveraget::compute_overall_coverage(
313315
{
314316
if(!gf_it->second.body_available() ||
315317
gf_it->first==goto_functions.entry_point() ||
316-
gf_it->first==CPROVER_PREFIX "initialize")
318+
gf_it->first == INITIALIZE_FUNCTION)
317319
continue;
318320

319321
goto_program_coverage_recordt func_cov(ns, gf_it, coverage);

‎src/cpp/cpp_internal_additions.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,8 @@ Author: Daniel Kroening, [email protected]
1414

1515
#include <ansi-c/ansi_c_internal_additions.h>
1616

17+
#include <linking/static_lifetime_init.h>
18+
1719
std::string c2cpp(const std::string &s)
1820
{
1921
std::string result;
@@ -75,7 +77,7 @@ void cpp_internal_additions(std::ostream &out)
7577

7678
// CPROVER extensions
7779
out << "extern \"C\" const unsigned __CPROVER::constant_infinity_uint;\n";
78-
out << "extern \"C\" void __CPROVER_initialize();" << '\n';
80+
out << "extern \"C\" void " INITIALIZE_FUNCTION "();" << '\n';
7981
out << "extern \"C\" void __CPROVER::input(const char *id, ...);" << '\n';
8082
out << "extern \"C\" void __CPROVER::output(const char *id, ...);" << '\n';
8183
out << "extern \"C\" void __CPROVER::cover(bool condition);" << '\n';

‎src/goto-cc/compile.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -41,6 +41,8 @@ Date: June 2006
4141

4242
#include <langapi/mode.h>
4343

44+
#include <linking/static_lifetime_init.h>
45+
4446
#include <cbmc/version.h>
4547

4648
#define DOTGRAPHSETTINGS "color=black;" \
@@ -372,7 +374,7 @@ bool compilet::link()
372374
// new symbols may have been added to a previously linked file
373375
// make sure a new entry point is created that contains all
374376
// static initializers
375-
compiled_functions.function_map.erase("__CPROVER_initialize");
377+
compiled_functions.function_map.erase(INITIALIZE_FUNCTION);
376378

377379
symbol_table.remove(goto_functionst::entry_point());
378380
compiled_functions.function_map.erase(goto_functionst::entry_point());

‎src/goto-cc/linker_script_merge.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@ Author: Kareem Khazem <[email protected]>, 2017
2424
#include <util/string2int.h>
2525
#include <util/tempfile.h>
2626

27+
#include <linking/static_lifetime_init.h>
2728
#include <linking/zero_initializer.h>
2829

2930
#include <goto-programs/read_goto_binary.h>
@@ -78,10 +79,10 @@ int linker_script_merget::add_linker_script_definitions()
7879

7980
fail=1;
8081
linker_valuest linker_values;
81-
const auto &pair=original_gf.function_map.find(CPROVER_PREFIX "initialize");
82+
const auto &pair=original_gf.function_map.find(INITIALIZE_FUNCTION);
8283
if(pair==original_gf.function_map.end())
8384
{
84-
error() << "No " << CPROVER_PREFIX "initialize found in goto_functions"
85+
error() << "No " << INITIALIZE_FUNCTION << " found in goto_functions"
8586
<< eom;
8687
return fail;
8788
}
@@ -93,7 +94,7 @@ int linker_script_merget::add_linker_script_definitions()
9394
linker_values);
9495
if(fail!=0)
9596
{
96-
error() << "Could not add linkerscript defs to __CPROVER_initialize" << eom;
97+
error() << "Could not add linkerscript defs to " INITIALIZE_FUNCTION << eom;
9798
return fail;
9899
}
99100

‎src/goto-instrument/call_sequences.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,8 @@ Date: April 2013
2424

2525
#include <langapi/language_util.h>
2626

27+
#include <linking/static_lifetime_init.h>
28+
2729
void show_call_sequences(
2830
const irep_idt &caller,
2931
const goto_programt &goto_program)
@@ -286,7 +288,7 @@ static void list_calls_and_arguments(
286288
continue;
287289

288290
const irep_idt &identifier=to_symbol_expr(f).get_identifier();
289-
if(identifier=="__CPROVER_initialize")
291+
if(identifier == INITIALIZE_FUNCTION)
290292
continue;
291293

292294
std::string name=from_expr(ns, identifier, f);

‎src/goto-instrument/code_contracts.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,8 @@ Date: February 2016
2121

2222
#include <analyses/local_may_alias.h>
2323

24+
#include <linking/static_lifetime_init.h>
25+
2426
#include "loop_utils.h"
2527

2628
class code_contractst
@@ -385,7 +387,7 @@ void code_contractst::operator()()
385387
code_contracts(it->second);
386388

387389
goto_functionst::function_mapt::iterator i_it=
388-
goto_functions.function_map.find(CPROVER_PREFIX "initialize");
390+
goto_functions.function_map.find(INITIALIZE_FUNCTION);
389391
assert(i_it!=goto_functions.function_map.end());
390392

391393
for(const auto &contract : summarized)

‎src/goto-instrument/cover_filter.cpp

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -11,9 +11,7 @@ Author: Peter Schrammel
1111

1212
#include "cover_filter.h"
1313

14-
#include <json/json_parser.h>
15-
16-
#include <util/message.h>
14+
#include <linking/static_lifetime_init.h>
1715

1816
/// Filter out functions that are not considered provided by the user
1917
/// \param identifier: a function name
@@ -26,7 +24,7 @@ bool internal_functions_filtert::operator()(
2624
if(identifier == goto_functionst::entry_point())
2725
return false;
2826

29-
if(identifier == (CPROVER_PREFIX "initialize"))
27+
if(identifier == INITIALIZE_FUNCTION)
3028
return false;
3129

3230
if(goto_function.is_hidden())

‎src/goto-instrument/dump_c.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,8 @@ Author: Daniel Kroening, [email protected]
2626
#include <ansi-c/ansi_c_language.h>
2727
#include <cpp/cpp_language.h>
2828

29+
#include <linking/static_lifetime_init.h>
30+
2931
#include "goto_program2code.h"
3032
#include "dump_c_class.h"
3133

@@ -953,7 +955,7 @@ void dump_ct::cleanup_harness(code_blockt &b)
953955
symbol_exprt &s=to_symbol_expr(func);
954956
if(s.get_identifier()==ID_main)
955957
s.set_identifier(CPROVER_PREFIX+id2string(ID_main));
956-
else if(s.get_identifier()==CPROVER_PREFIX "initialize")
958+
else if(s.get_identifier() == INITIALIZE_FUNCTION)
957959
continue;
958960
}
959961
}

‎src/goto-instrument/interrupt.cpp

Lines changed: 2 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -13,15 +13,7 @@ Date: September 2011
1313

1414
#include "interrupt.h"
1515

16-
#include <util/cprover_prefix.h>
17-
#include <util/std_expr.h>
18-
#include <util/std_code.h>
19-
#include <util/prefix.h>
20-
#include <util/symbol_table.h>
21-
22-
#include <goto-programs/goto_functions.h>
23-
24-
#include "rw_set.h"
16+
#include <linking/static_lifetime_init.h>
2517

2618
#ifdef LOCAL_MAY
2719
#include <analyses/local_may_alias.h>
@@ -203,7 +195,7 @@ void interrupt(
203195
// now instrument
204196

205197
Forall_goto_functions(f_it, goto_model.goto_functions)
206-
if(f_it->first!=CPROVER_PREFIX "initialize" &&
198+
if(f_it->first != INITIALIZE_FUNCTION &&
207199
f_it->first!=goto_functionst::entry_point() &&
208200
f_it->first!=isr.get_identifier())
209201
interrupt(

‎src/goto-instrument/mmio.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ Date: September 2011
1313

1414
#include "mmio.h"
1515

16-
#include <util/cprover_prefix.h>
16+
#include <linking/static_lifetime_init.h>
1717

1818
#include <goto-programs/goto_program.h>
1919
#include <goto-programs/goto_functions.h>
@@ -169,7 +169,7 @@ void mmio(
169169
// now instrument
170170

171171
Forall_goto_functions(f_it, goto_model.goto_functions)
172-
if(f_it->first!=CPROVER_PREFIX "initialize" &&
172+
if(f_it->first != INITIALIZE_FUNCTION &&
173173
f_it->first!=goto_functionst::entry_point())
174174
mmio(value_sets, goto_model.symbol_table,
175175
#ifdef LOCAL_MAY

‎src/goto-instrument/nondet_static.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,8 @@ Date: November 2011
2222
#include <goto-programs/goto_model.h>
2323
#include <goto-programs/goto_functions.h>
2424

25+
#include <linking/static_lifetime_init.h>
26+
2527
void nondet_static(
2628
const namespacet &ns,
2729
goto_functionst &goto_functions,
@@ -75,7 +77,7 @@ void nondet_static(
7577
const namespacet &ns,
7678
goto_functionst &goto_functions)
7779
{
78-
nondet_static(ns, goto_functions, CPROVER_PREFIX "initialize");
80+
nondet_static(ns, goto_functions, INITIALIZE_FUNCTION);
7981

8082
// update counters etc.
8183
goto_functions.update();

‎src/goto-instrument/race_check.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,8 @@ Date: February 2006
2525
#include <pointer-analysis/value_sets.h>
2626
#include <goto-programs/remove_skip.h>
2727

28+
#include <linking/static_lifetime_init.h>
29+
2830
#include "rw_set.h"
2931

3032
#ifdef LOCAL_MAY
@@ -300,7 +302,7 @@ void race_check(
300302

301303
Forall_goto_functions(f_it, goto_model.goto_functions)
302304
if(f_it->first!=goto_functionst::entry_point() &&
303-
f_it->first!=CPROVER_PREFIX "initialize")
305+
f_it->first != INITIALIZE_FUNCTION)
304306
race_check(
305307
value_sets,
306308
goto_model.symbol_table,

‎src/goto-instrument/stack_depth.cpp

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,8 @@ Date: November 2011
2222

2323
#include <goto-programs/goto_model.h>
2424

25+
#include <linking/static_lifetime_init.h>
26+
2527
symbol_exprt add_stack_depth_symbol(symbol_tablet &symbol_table)
2628
{
2729
const irep_idt identifier="$stack_depth";
@@ -94,17 +96,16 @@ void stack_depth(
9496

9597
Forall_goto_functions(f_it, goto_model.goto_functions)
9698
if(f_it->second.body_available() &&
97-
f_it->first!=CPROVER_PREFIX "initialize" &&
99+
f_it->first != INITIALIZE_FUNCTION &&
98100
f_it->first!=goto_functionst::entry_point())
99101
stack_depth(f_it->second.body, sym, depth, depth_expr);
100102

101103
// initialize depth to 0
102-
goto_functionst::function_mapt::iterator
103-
i_it=goto_model.goto_functions.function_map.find(
104-
CPROVER_PREFIX "initialize");
104+
goto_functionst::function_mapt::iterator i_it =
105+
goto_model.goto_functions.function_map.find(INITIALIZE_FUNCTION);
105106
DATA_INVARIANT(
106107
i_it!=goto_model.goto_functions.function_map.end(),
107-
"__CPROVER_initialize must exist");
108+
INITIALIZE_FUNCTION " must exist");
108109

109110
goto_programt &init=i_it->second.body;
110111
goto_programt::targett first=init.instructions.begin();

‎src/goto-instrument/wmm/goto2graph.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,8 @@ Date: 2012
2828
#include <util/message.h>
2929
#include <util/std_expr.h>
3030

31+
#include <linking/static_lifetime_init.h>
32+
3133
#include "../rw_set.h"
3234
#include "fence.h"
3335

@@ -168,7 +170,7 @@ void instrumentert::cfg_visitort::visit_cfg_function(
168170
instrumenter.message.debug() << "visit function "
169171
<< function << messaget::eom;
170172

171-
if(function==CPROVER_PREFIX "initialize")
173+
if(function == INITIALIZE_FUNCTION)
172174
{
173175
return;
174176
}

‎src/goto-instrument/wmm/shared_buffers.cpp

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,9 @@ Author: Daniel Kroening, [email protected]
77
\*******************************************************************/
88

99
#include "shared_buffers.h"
10+
11+
#include <linking/static_lifetime_init.h>
12+
1013
#include "fence.h"
1114
#include "../rw_set.h"
1215

@@ -1054,7 +1057,7 @@ void shared_bufferst::cfg_visitort::weak_memory(
10541057
{
10551058
shared_buffers.message.debug() << "visit function "<< function
10561059
<< messaget::eom;
1057-
if(function==CPROVER_PREFIX "initialize")
1060+
if(function == INITIALIZE_FUNCTION)
10581061
return;
10591062

10601063
namespacet ns(symbol_table);

‎src/goto-instrument/wmm/weak_memory.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,8 @@ Date: September 2011
2929

3030
#include <goto-programs/remove_skip.h>
3131

32+
#include <linking/static_lifetime_init.h>
33+
3234
#include "../rw_set.h"
3335

3436
#include "shared_buffers.h"
@@ -135,7 +137,7 @@ void weak_memory(
135137

136138
// all access to shared variables is pushed into assignments
137139
Forall_goto_functions(f_it, goto_model.goto_functions)
138-
if(f_it->first!=CPROVER_PREFIX "initialize" &&
140+
if(f_it->first != INITIALIZE_FUNCTION &&
139141
f_it->first!=goto_functionst::entry_point())
140142
introduce_temporaries(value_sets, goto_model.symbol_table, f_it->first,
141143
f_it->second.body,

‎src/java_bytecode/java_entry_point.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,8 @@ Author: Daniel Kroening, [email protected]
2929
#include <util/string_constant.h>
3030
#include <util/suffix.h>
3131

32-
#include "remove_exceptions.h"
32+
#include <linking/static_lifetime_init.h>
33+
3334
#include "java_object_factory.h"
3435
#include "java_types.h"
3536
#include "java_utils.h"

0 commit comments

Comments
 (0)