Skip to content

Commit 2af7929

Browse files
tautschnigtautschnig
committed
Rename zero_initializer to expr_initializer in preparation of generalisation
1 parent 1386e3f commit 2af7929

19 files changed

+42
-41
lines changed

‎jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,10 +23,10 @@ Author: Daniel Kroening, [email protected]
2323

2424
#include <util/arith_tools.h>
2525
#include <util/c_types.h>
26+
#include <util/expr_initializer.h>
2627
#include <util/namespace.h>
2728
#include <util/std_expr.h>
2829
#include <util/suffix.h>
29-
#include <util/zero_initializer.h>
3030

3131
class java_bytecode_convert_classt:public messaget
3232
{

‎jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,14 +24,14 @@ Author: Daniel Kroening, [email protected]
2424

2525
#include <util/arith_tools.h>
2626
#include <util/c_types.h>
27+
#include <util/expr_initializer.h>
2728
#include <util/ieee_float.h>
2829
#include <util/invariant.h>
2930
#include <util/namespace.h>
3031
#include <util/prefix.h>
3132
#include <util/simplify_expr.h>
3233
#include <util/std_expr.h>
3334
#include <util/string2int.h>
34-
#include <util/zero_initializer.h>
3535

3636
#include <goto-programs/cfg.h>
3737
#include <goto-programs/class_hierarchy.h>

‎jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,8 +12,8 @@ Author: Daniel Kroening, [email protected]
1212
#include "java_bytecode_typecheck.h"
1313

1414
#include <util/arith_tools.h>
15+
#include <util/expr_initializer.h>
1516
#include <util/unicode.h>
16-
#include <util/zero_initializer.h>
1717

1818
#include "java_pointer_casts.h"
1919
#include "java_types.h"

‎jbmc/src/java_bytecode/java_object_factory.cpp

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

99
#include "java_object_factory.h"
1010

11+
#include <util/expr_initializer.h>
1112
#include <util/fresh_symbol.h>
1213
#include <util/nondet_bool.h>
1314
#include <util/pointer_offset_size.h>
14-
#include <util/zero_initializer.h>
1515

1616
#include <goto-programs/class_identifier.h>
1717
#include <goto-programs/goto_functions.h>

‎jbmc/src/java_bytecode/java_string_literals.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,9 +12,9 @@ Author: Chris Smowton, [email protected]
1212
#include "java_utils.h"
1313

1414
#include <util/arith_tools.h>
15+
#include <util/expr_initializer.h>
1516
#include <util/namespace.h>
1617
#include <util/unicode.h>
17-
#include <util/zero_initializer.h>
1818

1919
#include <iomanip>
2020
#include <sstream>

‎jbmc/src/java_bytecode/remove_java_new.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,10 +17,10 @@ Author: Peter Schrammel
1717
#include <util/arith_tools.h>
1818
#include <util/c_types.h>
1919
#include <util/expr_cast.h>
20+
#include <util/expr_initializer.h>
2021
#include <util/fresh_symbol.h>
2122
#include <util/message.h>
2223
#include <util/pointer_offset_size.h>
23-
#include <util/zero_initializer.h>
2424

2525
class remove_java_newt : public messaget
2626
{

‎src/ansi-c/c_typecheck_code.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +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>
15+
#include <util/expr_initializer.h>
1616

1717
#include "ansi_c_declaration.h"
1818

‎src/ansi-c/c_typecheck_initializer.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,12 +14,12 @@ Author: Daniel Kroening, [email protected]
1414
#include <util/arith_tools.h>
1515
#include <util/c_types.h>
1616
#include <util/cprover_prefix.h>
17+
#include <util/expr_initializer.h>
1718
#include <util/prefix.h>
1819
#include <util/simplify_expr.h>
1920
#include <util/std_types.h>
2021
#include <util/string_constant.h>
2122
#include <util/type_eq.h>
22-
#include <util/zero_initializer.h>
2323

2424
#include "anonymous_member.h"
2525

‎src/cpp/cpp_typecheck.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,9 +14,9 @@ Author: Daniel Kroening, [email protected]
1414
#include <algorithm>
1515

1616
#include <util/arith_tools.h>
17+
#include <util/expr_initializer.h>
1718
#include <util/source_location.h>
1819
#include <util/symbol.h>
19-
#include <util/zero_initializer.h>
2020

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

‎src/cpp/cpp_typecheck_expr.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,8 +19,8 @@ Author: Daniel Kroening, [email protected]
1919
#include <util/base_type.h>
2020
#include <util/c_types.h>
2121
#include <util/config.h>
22+
#include <util/expr_initializer.h>
2223
#include <util/pointer_offset_size.h>
23-
#include <util/zero_initializer.h>
2424

2525
#include <ansi-c/c_qualifiers.h>
2626

‎src/cpp/cpp_typecheck_initializer.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,8 +13,8 @@ Author: Daniel Kroening, [email protected]
1313

1414
#include <util/arith_tools.h>
1515
#include <util/c_types.h>
16+
#include <util/expr_initializer.h>
1617
#include <util/pointer_offset_size.h>
17-
#include <util/zero_initializer.h>
1818

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

‎src/goto-cc/linker_script_merge.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,10 +14,10 @@ Author: Kareem Khazem <[email protected]>, 2017
1414

1515
#include <util/arith_tools.h>
1616
#include <util/c_types.h>
17+
#include <util/expr_initializer.h>
1718
#include <util/magic.h>
1819
#include <util/run.h>
1920
#include <util/tempfile.h>
20-
#include <util/zero_initializer.h>
2121

2222
#include <json/json_parser.h>
2323

‎src/goto-programs/builtin_functions.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,10 +16,10 @@ Author: Daniel Kroening, [email protected]
1616
#include <util/arith_tools.h>
1717
#include <util/c_types.h>
1818
#include <util/cprover_prefix.h>
19+
#include <util/expr_initializer.h>
1920
#include <util/pointer_offset_size.h>
2021
#include <util/rational.h>
2122
#include <util/rational_tools.h>
22-
#include <util/zero_initializer.h>
2323

2424
#include <langapi/language_util.h>
2525

‎src/goto-symex/symex_builtin_functions.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,11 +13,11 @@ Author: Daniel Kroening, [email protected]
1313

1414
#include <util/arith_tools.h>
1515
#include <util/c_types.h>
16+
#include <util/expr_initializer.h>
1617
#include <util/invariant_utils.h>
1718
#include <util/pointer_offset_size.h>
1819
#include <util/simplify_expr.h>
1920
#include <util/string2int.h>
20-
#include <util/zero_initializer.h>
2121

2222
inline static typet c_sizeof_type_rec(const exprt &expr)
2323
{

‎src/goto-symex/symex_start_thread.cpp

Lines changed: 1 addition & 1 deletion
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 <util/zero_initializer.h>
14+
#include <util/expr_initializer.h>
1515

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

‎src/linking/static_lifetime_init.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,11 +14,11 @@ Author: Daniel Kroening, [email protected]
1414
#include <util/arith_tools.h>
1515
#include <util/c_types.h>
1616
#include <util/config.h>
17+
#include <util/expr_initializer.h>
1718
#include <util/namespace.h>
1819
#include <util/prefix.h>
1920
#include <util/std_code.h>
2021
#include <util/std_expr.h>
21-
#include <util/zero_initializer.h>
2222

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

‎src/util/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ SRC = arith_tools.cpp \
1111
dstring.cpp \
1212
endianness_map.cpp \
1313
expr.cpp \
14+
expr_initializer.cpp \
1415
expr_util.cpp \
1516
file_util.cpp \
1617
find_macros.cpp \
@@ -98,7 +99,6 @@ SRC = arith_tools.cpp \
9899
xml.cpp \
99100
xml_expr.cpp \
100101
xml_irep.cpp \
101-
zero_initializer.cpp \
102102
# Empty last line
103103

104104
INCLUDES= -I ..

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

Lines changed: 20 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,15 @@
11
/*******************************************************************\
22
3-
Module: Zero Initialization
3+
Module: Expression Initialization
44
55
Author: Daniel Kroening, [email protected]
66
77
\*******************************************************************/
88

99
/// \file
10-
/// Zero Initialization
10+
/// Expression Initialization
1111

12-
#include "zero_initializer.h"
12+
#include "expr_initializer.h"
1313

1414
#include "arith_tools.h"
1515
#include "c_types.h"
@@ -20,10 +20,10 @@ Author: Daniel Kroening, [email protected]
2020
#include "pointer_offset_size.h"
2121
#include "std_expr.h"
2222

23-
class zero_initializert:public messaget
23+
class expr_initializert : public messaget
2424
{
2525
public:
26-
zero_initializert(
26+
expr_initializert(
2727
const namespacet &_ns,
2828
message_handlert &_message_handler):
2929
messaget(_message_handler),
@@ -35,18 +35,18 @@ class zero_initializert:public messaget
3535
const typet &type,
3636
const source_locationt &source_location)
3737
{
38-
return zero_initializer_rec(type, source_location);
38+
return expr_initializer_rec(type, source_location);
3939
}
4040

4141
protected:
4242
const namespacet &ns;
4343

44-
exprt zero_initializer_rec(
44+
exprt expr_initializer_rec(
4545
const typet &type,
4646
const source_locationt &source_location);
4747
};
4848

49-
exprt zero_initializert::zero_initializer_rec(
49+
exprt expr_initializert::expr_initializer_rec(
5050
const typet &type,
5151
const source_locationt &source_location)
5252
{
@@ -86,7 +86,7 @@ exprt zero_initializert::zero_initializer_rec(
8686
}
8787
else if(type_id==ID_complex)
8888
{
89-
exprt sub_zero=zero_initializer_rec(type.subtype(), source_location);
89+
exprt sub_zero = expr_initializer_rec(type.subtype(), source_location);
9090
complex_exprt result(sub_zero, sub_zero, to_complex_type(type));
9191
result.add_source_location()=source_location;
9292
return result;
@@ -113,7 +113,8 @@ exprt zero_initializert::zero_initializer_rec(
113113
}
114114
else
115115
{
116-
exprt tmpval=zero_initializer_rec(array_type.subtype(), source_location);
116+
exprt tmpval =
117+
expr_initializer_rec(array_type.subtype(), source_location);
117118

118119
mp_integer array_size;
119120

@@ -148,7 +149,7 @@ exprt zero_initializert::zero_initializer_rec(
148149
{
149150
const vector_typet &vector_type=to_vector_type(type);
150151

151-
exprt tmpval=zero_initializer_rec(vector_type.subtype(), source_location);
152+
exprt tmpval = expr_initializer_rec(vector_type.subtype(), source_location);
152153

153154
mp_integer vector_size;
154155

@@ -195,7 +196,7 @@ exprt zero_initializert::zero_initializer_rec(
195196
}
196197
else
197198
value.copy_to_operands(
198-
zero_initializer_rec(it->type(), source_location));
199+
expr_initializer_rec(it->type(), source_location));
199200
}
200201

201202
value.add_source_location()=source_location;
@@ -245,14 +246,14 @@ exprt zero_initializert::zero_initializer_rec(
245246
{
246247
value.set_component_name(component.get_name());
247248
value.op()=
248-
zero_initializer_rec(component.type(), source_location);
249+
expr_initializer_rec(component.type(), source_location);
249250
}
250251

251252
return value;
252253
}
253254
else if(type_id==ID_symbol)
254255
{
255-
exprt result=zero_initializer_rec(ns.follow(type), source_location);
256+
exprt result = expr_initializer_rec(ns.follow(type), source_location);
256257
// we might have mangled the type for arrays, so keep that
257258
if(ns.follow(type).id()!=ID_array)
258259
result.type()=type;
@@ -262,21 +263,21 @@ exprt zero_initializert::zero_initializer_rec(
262263
else if(type_id==ID_c_enum_tag)
263264
{
264265
return
265-
zero_initializer_rec(
266+
expr_initializer_rec(
266267
ns.follow_tag(to_c_enum_tag_type(type)),
267268
source_location);
268269
}
269270
else if(type_id==ID_struct_tag)
270271
{
271272
return
272-
zero_initializer_rec(
273+
expr_initializer_rec(
273274
ns.follow_tag(to_struct_tag_type(type)),
274275
source_location);
275276
}
276277
else if(type_id==ID_union_tag)
277278
{
278279
return
279-
zero_initializer_rec(
280+
expr_initializer_rec(
280281
ns.follow_tag(to_union_tag_type(type)),
281282
source_location);
282283
}
@@ -298,7 +299,7 @@ exprt zero_initializer(
298299
const namespacet &ns,
299300
message_handlert &message_handler)
300301
{
301-
zero_initializert z_i(ns, message_handler);
302+
expr_initializert z_i(ns, message_handler);
302303
return z_i(type, source_location);
303304
}
304305

@@ -312,7 +313,7 @@ exprt zero_initializer(
312313

313314
try
314315
{
315-
zero_initializert z_i(ns, mh);
316+
expr_initializert z_i(ns, mh);
316317
return z_i(type, source_location);
317318
}
318319
catch(int)

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

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,16 @@
11
/*******************************************************************\
22
3-
Module: Zero Initialization
3+
Module: Expression Initialization
44
55
Author: Daniel Kroening, [email protected]
66
77
\*******************************************************************/
88

99
/// \file
10-
/// Zero Initialization
10+
/// Expression Initialization
1111

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

1515
#include "expr.h"
1616

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

33-
#endif // CPROVER_UTIL_ZERO_INITIALIZER_H
33+
#endif // CPROVER_UTIL_EXPR_INITIALIZER_H

0 commit comments

Comments
 (0)