Skip to content

Commit bc15b1b

Browse files
tautschnigtautschnig
committed
Move zero_initializer to util
This is really just expression-generating code, it isn't specific to linking in any way. Get rid of the dependency on ansi-c/expr2c by using format().
1 parent 2ed63f5 commit bc15b1b

22 files changed

+44
-70
lines changed

‎jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

+2-3
Original file line numberDiff line numberDiff line change
@@ -21,13 +21,12 @@ Author: Daniel Kroening, [email protected]
2121
#include "java_bytecode_language.h"
2222
#include "java_utils.h"
2323

24-
#include <util/c_types.h>
2524
#include <util/arith_tools.h>
25+
#include <util/c_types.h>
2626
#include <util/namespace.h>
2727
#include <util/std_expr.h>
28-
29-
#include <linking/zero_initializer.h>
3028
#include <util/suffix.h>
29+
#include <util/zero_initializer.h>
3130

3231
class java_bytecode_convert_classt:public messaget
3332
{

‎jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

+1-2
Original file line numberDiff line numberDiff line change
@@ -31,8 +31,7 @@ Author: Daniel Kroening, [email protected]
3131
#include <util/simplify_expr.h>
3232
#include <util/std_expr.h>
3333
#include <util/string2int.h>
34-
35-
#include <linking/zero_initializer.h>
34+
#include <util/zero_initializer.h>
3635

3736
#include <goto-programs/cfg.h>
3837
#include <goto-programs/class_hierarchy.h>

‎jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp

+1-2
Original file line numberDiff line numberDiff line change
@@ -13,8 +13,7 @@ Author: Daniel Kroening, [email protected]
1313

1414
#include <util/arith_tools.h>
1515
#include <util/unicode.h>
16-
17-
#include <linking/zero_initializer.h>
16+
#include <util/zero_initializer.h>
1817

1918
#include "java_pointer_casts.h"
2019
#include "java_types.h"

‎jbmc/src/java_bytecode/java_object_factory.cpp

+1-2
Original file line numberDiff line numberDiff line change
@@ -11,12 +11,11 @@ Author: Daniel Kroening, [email protected]
1111
#include <util/fresh_symbol.h>
1212
#include <util/nondet_bool.h>
1313
#include <util/pointer_offset_size.h>
14+
#include <util/zero_initializer.h>
1415

1516
#include <goto-programs/class_identifier.h>
1617
#include <goto-programs/goto_functions.h>
1718

18-
#include <linking/zero_initializer.h>
19-
2019
#include "generic_parameter_specialization_map_keys.h"
2120
#include "java_root_class.h"
2221

‎jbmc/src/java_bytecode/java_string_literals.cpp

+1-2
Original file line numberDiff line numberDiff line change
@@ -11,11 +11,10 @@ Author: Chris Smowton, [email protected]
1111
#include "java_types.h"
1212
#include "java_utils.h"
1313

14-
#include <linking/zero_initializer.h>
15-
1614
#include <util/arith_tools.h>
1715
#include <util/namespace.h>
1816
#include <util/unicode.h>
17+
#include <util/zero_initializer.h>
1918

2019
#include <iomanip>
2120
#include <sstream>

‎jbmc/src/java_bytecode/remove_java_new.cpp

+1-2
Original file line numberDiff line numberDiff line change
@@ -14,14 +14,13 @@ Author: Peter Schrammel
1414
#include <goto-programs/class_identifier.h>
1515
#include <goto-programs/goto_convert.h>
1616

17-
#include <linking/zero_initializer.h>
18-
1917
#include <util/arith_tools.h>
2018
#include <util/c_types.h>
2119
#include <util/expr_cast.h>
2220
#include <util/fresh_symbol.h>
2321
#include <util/message.h>
2422
#include <util/pointer_offset_size.h>
23+
#include <util/zero_initializer.h>
2524

2625
class remove_java_newt : public messaget
2726
{

‎src/ansi-c/c_typecheck_code.cpp

+1
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
1212
#include "c_typecheck_base.h"
1313

1414
#include <util/config.h>
15+
#include <util/zero_initializer.h>
1516

1617
#include "ansi_c_declaration.h"
1718

‎src/ansi-c/c_typecheck_initializer.cpp

+1-2
Original file line numberDiff line numberDiff line change
@@ -19,8 +19,7 @@ Author: Daniel Kroening, [email protected]
1919
#include <util/std_types.h>
2020
#include <util/string_constant.h>
2121
#include <util/type_eq.h>
22-
23-
#include <linking/zero_initializer.h>
22+
#include <util/zero_initializer.h>
2423

2524
#include "anonymous_member.h"
2625

‎src/cpp/cpp_typecheck.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -16,8 +16,8 @@ Author: Daniel Kroening, [email protected]
1616
#include <util/arith_tools.h>
1717
#include <util/source_location.h>
1818
#include <util/symbol.h>
19+
#include <util/zero_initializer.h>
1920

20-
#include <linking/zero_initializer.h>
2121
#include <ansi-c/c_typecast.h>
2222

2323
#include "expr2cpp.h"

‎src/cpp/cpp_typecheck_expr.cpp

+1-2
Original file line numberDiff line numberDiff line change
@@ -20,11 +20,10 @@ Author: Daniel Kroening, [email protected]
2020
#include <util/c_types.h>
2121
#include <util/config.h>
2222
#include <util/pointer_offset_size.h>
23+
#include <util/zero_initializer.h>
2324

2425
#include <ansi-c/c_qualifiers.h>
2526

26-
#include <linking/zero_initializer.h>
27-
2827
#include "cpp_exception_id.h"
2928
#include "cpp_type2name.h"
3029
#include "expr2cpp.h"

‎src/cpp/cpp_typecheck_initializer.cpp

+1-2
Original file line numberDiff line numberDiff line change
@@ -14,8 +14,7 @@ Author: Daniel Kroening, [email protected]
1414
#include <util/arith_tools.h>
1515
#include <util/c_types.h>
1616
#include <util/pointer_offset_size.h>
17-
18-
#include <linking/zero_initializer.h>
17+
#include <util/zero_initializer.h>
1918

2019
/// Initialize an object with a value
2120
void cpp_typecheckt::convert_initializer(symbolt &symbol)

‎src/goto-cc/linker_script_merge.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -17,11 +17,11 @@ Author: Kareem Khazem <[email protected]>, 2017
1717
#include <util/magic.h>
1818
#include <util/run.h>
1919
#include <util/tempfile.h>
20+
#include <util/zero_initializer.h>
2021

2122
#include <json/json_parser.h>
2223

2324
#include <linking/static_lifetime_init.h>
24-
#include <linking/zero_initializer.h>
2525

2626
#include <goto-programs/read_goto_binary.h>
2727

‎src/goto-programs/builtin_functions.cpp

+1-2
Original file line numberDiff line numberDiff line change
@@ -19,8 +19,7 @@ Author: Daniel Kroening, [email protected]
1919
#include <util/pointer_offset_size.h>
2020
#include <util/rational.h>
2121
#include <util/rational_tools.h>
22-
23-
#include <linking/zero_initializer.h>
22+
#include <util/zero_initializer.h>
2423

2524
#include <langapi/language_util.h>
2625

‎src/goto-symex/symex_builtin_functions.cpp

+1-2
Original file line numberDiff line numberDiff line change
@@ -17,8 +17,7 @@ Author: Daniel Kroening, [email protected]
1717
#include <util/pointer_offset_size.h>
1818
#include <util/simplify_expr.h>
1919
#include <util/string2int.h>
20-
21-
#include <linking/zero_initializer.h>
20+
#include <util/zero_initializer.h>
2221

2322
inline static typet c_sizeof_type_rec(const exprt &expr)
2423
{

‎src/goto-symex/symex_start_thread.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ Author: Daniel Kroening, [email protected]
1111

1212
#include "goto_symex.h"
1313

14-
#include <linking/zero_initializer.h>
14+
#include <util/zero_initializer.h>
1515

1616
void goto_symext::symex_start_thread(statet &state)
1717
{

‎src/linking/CMakeLists.txt

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,4 +3,4 @@ add_library(linking ${sources})
33

44
generic_includes(linking)
55

6-
target_link_libraries(linking util ansi-c)
6+
target_link_libraries(linking util)

‎src/linking/Makefile

-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
SRC = linking.cpp \
22
remove_internal_symbols.cpp \
33
static_lifetime_init.cpp \
4-
zero_initializer.cpp \
54
# Empty last line
65

76
INCLUDES= -I ..

‎src/linking/module_dependencies.txt

-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
ansi-c # should go away
21
goto-programs
32
langapi # should go away
43
linking

‎src/linking/static_lifetime_init.cpp

+5-7
Original file line numberDiff line numberDiff line change
@@ -11,19 +11,17 @@ Author: Daniel Kroening, [email protected]
1111
#include <cassert>
1212
#include <cstdlib>
1313

14-
#include <util/namespace.h>
15-
#include <util/std_expr.h>
1614
#include <util/arith_tools.h>
17-
#include <util/std_code.h>
15+
#include <util/c_types.h>
1816
#include <util/config.h>
17+
#include <util/namespace.h>
1918
#include <util/prefix.h>
20-
21-
#include <util/c_types.h>
19+
#include <util/std_code.h>
20+
#include <util/std_expr.h>
21+
#include <util/zero_initializer.h>
2222

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

25-
#include "zero_initializer.h"
26-
2725
bool static_lifetime_init(
2826
symbol_tablet &symbol_table,
2927
const source_locationt &source_location,

‎src/util/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -98,6 +98,7 @@ SRC = arith_tools.cpp \
9898
xml.cpp \
9999
xml_expr.cpp \
100100
xml_irep.cpp \
101+
zero_initializer.cpp \
101102
# Empty last line
102103

103104
INCLUDES= -I ..

‎src/linking/zero_initializer.cpp renamed to ‎src/util/zero_initializer.cpp

+15-28
Original file line numberDiff line numberDiff line change
@@ -1,24 +1,24 @@
11
/*******************************************************************\
22
3-
Module: Linking: Zero Initialization
3+
Module: Zero Initialization
44
55
Author: Daniel Kroening, [email protected]
66
77
\*******************************************************************/
88

99
/// \file
10-
/// Linking: Zero Initialization
10+
/// Zero Initialization
1111

1212
#include "zero_initializer.h"
1313

14-
#include <util/arith_tools.h>
15-
#include <util/c_types.h>
16-
#include <util/message.h>
17-
#include <util/namespace.h>
18-
#include <util/pointer_offset_size.h>
19-
#include <util/std_expr.h>
20-
21-
#include <ansi-c/expr2c.h>
14+
#include "arith_tools.h"
15+
#include "c_types.h"
16+
#include "format_expr.h"
17+
#include "format_type.h"
18+
#include "message.h"
19+
#include "namespace.h"
20+
#include "pointer_offset_size.h"
21+
#include "std_expr.h"
2222

2323
class zero_initializert:public messaget
2424
{
@@ -41,16 +41,6 @@ class zero_initializert:public messaget
4141
protected:
4242
const namespacet &ns;
4343

44-
std::string to_string(const exprt &src)
45-
{
46-
return expr2c(src, ns);
47-
}
48-
49-
std::string to_string(const typet &src)
50-
{
51-
return type2c(src, ns);
52-
}
53-
5444
exprt zero_initializer_rec(
5545
const typet &type,
5646
const source_locationt &source_location);
@@ -137,15 +127,14 @@ exprt zero_initializert::zero_initializer_rec(
137127
{
138128
error().source_location=source_location;
139129
error() << "failed to zero-initialize array of non-fixed size `"
140-
<< to_string(array_type.size()) << "'" << eom;
130+
<< format(array_type.size()) << "'" << eom;
141131
throw 0;
142132
}
143133

144134
if(array_size<0)
145135
{
146136
error().source_location=source_location;
147-
error() << "failed to zero-initialize array of with negative size"
148-
<< eom;
137+
error() << "failed to zero-initialize array with negative size" << eom;
149138
throw 0;
150139
}
151140

@@ -167,15 +156,14 @@ exprt zero_initializert::zero_initializer_rec(
167156
{
168157
error().source_location=source_location;
169158
error() << "failed to zero-initialize vector of non-fixed size `"
170-
<< to_string(vector_type.size()) << "'" << eom;
159+
<< format(vector_type.size()) << "'" << eom;
171160
throw 0;
172161
}
173162

174163
if(vector_size<0)
175164
{
176165
error().source_location=source_location;
177-
error() << "failed to zero-initialize vector of with negative size"
178-
<< eom;
166+
error() << "failed to zero-initialize vector with negative size" << eom;
179167
throw 0;
180168
}
181169

@@ -299,8 +287,7 @@ exprt zero_initializert::zero_initializer_rec(
299287
else
300288
{
301289
error().source_location=source_location;
302-
error() << "failed to zero-initialize `" << to_string(type)
303-
<< "'" << eom;
290+
error() << "failed to zero-initialize `" << format(type) << "'" << eom;
304291
throw 0;
305292
}
306293
}

‎src/linking/zero_initializer.h renamed to ‎src/util/zero_initializer.h

+6-6
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,18 @@
11
/*******************************************************************\
22
3-
Module: Linking: Zero Initialization
3+
Module: Zero Initialization
44
55
Author: Daniel Kroening, [email protected]
66
77
\*******************************************************************/
88

99
/// \file
10-
/// Linking: Zero Initialization
10+
/// Zero Initialization
1111

12-
#ifndef CPROVER_LINKING_ZERO_INITIALIZER_H
13-
#define CPROVER_LINKING_ZERO_INITIALIZER_H
12+
#ifndef CPROVER_UTIL_ZERO_INITIALIZER_H
13+
#define CPROVER_UTIL_ZERO_INITIALIZER_H
1414

15-
#include <util/expr.h>
15+
#include "expr.h"
1616

1717
class message_handlert;
1818
class namespacet;
@@ -30,4 +30,4 @@ exprt zero_initializer(
3030
const source_locationt &,
3131
const namespacet &);
3232

33-
#endif // CPROVER_LINKING_ZERO_INITIALIZER_H
33+
#endif // CPROVER_UTIL_ZERO_INITIALIZER_H

0 commit comments

Comments
 (0)