Skip to content

Commit b4427d1

Browse files
authored
Merge pull request #5668 from martin-cs/fix/use-initializer-macro
Use the macro from linking/ rather than repeating the definition
2 parents ccbf14d + a77fd31 commit b4427d1

File tree

2 files changed

+4
-4
lines changed

2 files changed

+4
-4
lines changed

src/goto-programs/add_malloc_may_fail_variable_initializations.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,8 @@
55

66
#include "goto_model.h"
77

8+
#include <linking/static_lifetime_init.h>
9+
810
#include <util/arith_tools.h>
911
#include <util/config.h>
1012
#include <util/irep.h>
@@ -36,7 +38,7 @@ void add_malloc_may_fail_variable_initializations(goto_modelt &goto_model)
3638
"if malloc_may_fail is in the symbol table then so should "
3739
"malloc_failure_mode");
3840

39-
auto const initialize_function_name = CPROVER_PREFIX "initialize";
41+
auto const initialize_function_name = INITIALIZE_FUNCTION;
4042
PRECONDITION(
4143
goto_model.get_goto_functions().function_map.count(
4244
initialize_function_name) == 1);

src/statement-list/statement_list_entry_point.cpp

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -13,13 +13,11 @@ Author: Matthias Weiss, [email protected]
1313
#include "statement_list_typecheck.h"
1414

1515
#include <goto-programs/goto_functions.h>
16+
#include <linking/static_lifetime_init.h>
1617
#include <util/c_types.h>
1718
#include <util/config.h>
1819
#include <util/std_code.h>
1920

20-
/// Name of the CPROVER-specific function that initializes static variables.
21-
#define INITIALIZE_FUNCTION CPROVER_PREFIX "initialize"
22-
2321
/// Name of the CPROVER-specific variable that specifies the rounding mode.
2422
#define ROUNDING_MODE_NAME CPROVER_PREFIX "rounding_mode"
2523

0 commit comments

Comments
 (0)