Skip to content

Commit 341c1a0

Browse files
author
martin
committed
Use the macro from linking/ rather than repeating the definition
1 parent c9c3ca6 commit 341c1a0

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>
@@ -21,7 +23,7 @@ code_assignt make_integer_assignment(
2123

2224
void add_malloc_may_fail_variable_initializations(goto_modelt &goto_model)
2325
{
24-
const auto malloc_may_fail_id = irep_idt{CPROVER_PREFIX "malloc_may_fail"};
26+
const auto malloc_may_fail_id = irep_idt{INITIALIZE_FUNCTION};
2527
const auto malloc_failure_mode_id =
2628
irep_idt{CPROVER_PREFIX "malloc_failure_mode"};
2729
if(!goto_model.symbol_table.has_symbol(malloc_may_fail_id))

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)