Skip to content

Commit 087296a

Browse files
tautschnigtautschnig
authored
Merge pull request #6577 from diffblue/c_index_type
rename index_type and enum_constant_type
2 parents 5887174 + 4271a0a commit 087296a

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

41 files changed

+131
-122
lines changed

‎src/analyses/local_may_alias.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -217,7 +217,7 @@ void local_may_aliast::get_rec(
217217
if(index_expr.array().id()==ID_symbol)
218218
{
219219
index_exprt tmp1=index_expr;
220-
tmp1.index()=from_integer(0, index_type());
220+
tmp1.index() = from_integer(0, c_index_type());
221221
address_of_exprt tmp2(tmp1);
222222
unsigned object_nr=objects.number(tmp2);
223223
dest.insert(object_nr);
@@ -229,7 +229,7 @@ void local_may_aliast::get_rec(
229229
else if(index_expr.array().id()==ID_string_constant)
230230
{
231231
index_exprt tmp1=index_expr;
232-
tmp1.index()=from_integer(0, index_type());
232+
tmp1.index() = from_integer(0, c_index_type());
233233
address_of_exprt tmp2(tmp1);
234234
unsigned object_nr=objects.number(tmp2);
235235
dest.insert(object_nr);

‎src/ansi-c/ansi_c_entry_point.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -448,7 +448,7 @@ bool generate_ansi_c_start_function(
448448

449449
{
450450
index_exprt index_expr(
451-
argv_symbol.symbol_expr(), from_integer(0, index_type()));
451+
argv_symbol.symbol_expr(), from_integer(0, c_index_type()));
452452

453453
// disable bounds check on that one
454454
index_expr.set(ID_C_bounds_check, false);
@@ -466,7 +466,7 @@ bool generate_ansi_c_start_function(
466466
const symbolt &envp_symbol=ns.lookup("envp'");
467467

468468
index_exprt index_expr(
469-
envp_symbol.symbol_expr(), from_integer(0, index_type()));
469+
envp_symbol.symbol_expr(), from_integer(0, c_index_type()));
470470

471471
const pointer_typet &pointer_type =
472472
to_pointer_type(parameters[2].type());

‎src/ansi-c/c_typecast.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -722,7 +722,7 @@ void c_typecastt::do_typecast(exprt &expr, const typet &dest_type)
722722

723723
if(src_type.id()==ID_array)
724724
{
725-
index_exprt index(expr, from_integer(0, index_type()));
725+
index_exprt index(expr, from_integer(0, c_index_type()));
726726
expr = typecast_exprt::conditional_cast(address_of_exprt(index), dest_type);
727727
return;
728728
}

‎src/ansi-c/c_typecheck_expr.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1185,7 +1185,7 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr)
11851185
}
11861186
else if(op_type.id()==ID_array)
11871187
{
1188-
index_exprt index(op, from_integer(0, index_type()));
1188+
index_exprt index(op, from_integer(0, c_index_type()));
11891189
op=address_of_exprt(index);
11901190
}
11911191
else if(op_type.id()==ID_empty)
@@ -1245,7 +1245,7 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr)
12451245

12461246
void c_typecheck_baset::make_index_type(exprt &expr)
12471247
{
1248-
implicit_typecast(expr, index_type());
1248+
implicit_typecast(expr, c_index_type());
12491249
}
12501250

12511251
void c_typecheck_baset::typecheck_expr_index(exprt &expr)
@@ -1456,7 +1456,7 @@ void c_typecheck_baset::typecheck_expr_ptrmember(exprt &expr)
14561456
if(op0_type.id() == ID_array)
14571457
{
14581458
// a->f is the same as a[0].f
1459-
exprt zero=from_integer(0, index_type());
1459+
exprt zero = from_integer(0, c_index_type());
14601460
index_exprt index_expr(op, zero, op0_type.subtype());
14611461
index_expr.set(ID_C_lvalue, true);
14621462
op.swap(index_expr);
@@ -1774,7 +1774,7 @@ void c_typecheck_baset::typecheck_expr_dereference(exprt &expr)
17741774
// *a is the same as a[0]
17751775
expr.id(ID_index);
17761776
expr.type()=op_type.subtype();
1777-
expr.copy_to_operands(from_integer(0, index_type()));
1777+
expr.copy_to_operands(from_integer(0, c_index_type()));
17781778
assert(expr.operands().size()==2);
17791779
}
17801780
else if(op_type.id()==ID_pointer)

‎src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1445,7 +1445,7 @@ exprt c_typecheck_baset::typecheck_shuffle_vector(
14451445
for(std::size_t i = 0; i < indices_size; ++i)
14461446
{
14471447
// only the least significant bits of each mask element are considered
1448-
mod_exprt mod_index{index_exprt{indices, from_integer(i, index_type())},
1448+
mod_exprt mod_index{index_exprt{indices, from_integer(i, c_index_type())},
14491449
size};
14501450
mod_index.add_source_location() = source_location;
14511451
operands.push_back(std::move(mod_index));

‎src/ansi-c/c_typecheck_initializer.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -542,7 +542,7 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
542542
if(current_symbol.is_static_lifetime)
543543
{
544544
byte_update_exprt byte_update =
545-
make_byte_update(*dest, from_integer(0, index_type()), *zero);
545+
make_byte_update(*dest, from_integer(0, c_index_type()), *zero);
546546
byte_update.add_source_location() = value.source_location();
547547
*dest = std::move(byte_update);
548548
dest = &(to_byte_update_expr(*dest).op2());
@@ -1029,7 +1029,7 @@ exprt c_typecheck_baset::do_initializer_list(
10291029
// make complete by setting array size
10301030
size_t size=result.operands().size();
10311031
result.type().id(ID_array);
1032-
result.type().set(ID_size, from_integer(size, index_type()));
1032+
result.type().set(ID_size, from_integer(size, c_index_type()));
10331033
}
10341034

10351035
return result;

‎src/ansi-c/c_typecheck_type.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1011,7 +1011,7 @@ void c_typecheck_baset::typecheck_compound_body(
10111011

10121012
// make it zero-length
10131013
c_type.id(ID_array);
1014-
c_type.set(ID_size, from_integer(0, index_type()));
1014+
c_type.set(ID_size, from_integer(0, c_index_type()));
10151015
}
10161016
}
10171017
}

‎src/ansi-c/literals/convert_string_literal.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -127,7 +127,7 @@ exprt convert_string_literal(const std::string &src)
127127
result.set(ID_C_string_constant, true);
128128
result.type()=typet(ID_array);
129129
result.type().subtype()=subtype;
130-
result.type().set(ID_size, from_integer(value.size(), index_type()));
130+
result.type().set(ID_size, from_integer(value.size(), c_index_type()));
131131

132132
result.operands().resize(value.size());
133133
for(std::size_t i=0; i<value.size(); i++)

‎src/cpp/cpp_constructor.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -97,7 +97,7 @@ optionalt<codet> cpp_typecheckt::cpp_constructor(
9797
{
9898
exprt::operandst tmp_operands;
9999

100-
exprt constant=from_integer(i, index_type());
100+
exprt constant = from_integer(i, c_index_type());
101101
constant.add_source_location()=source_location;
102102

103103
index_exprt index(object, constant);

‎src/cpp/cpp_destructor.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -56,7 +56,7 @@ optionalt<codet> cpp_typecheckt::cpp_destructor(
5656
// for each element of the array, call the destructor
5757
for(mp_integer i=0; i < s; ++i)
5858
{
59-
exprt constant=from_integer(i, index_type());
59+
exprt constant = from_integer(i, c_index_type());
6060
constant.add_source_location()=source_location;
6161

6262
index_exprt index(object, constant);

‎src/cpp/cpp_typecheck_constructor.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -90,7 +90,7 @@ static void copy_array(
9090
exprt &block)
9191
{
9292
// Build the index expression
93-
const exprt constant = from_integer(i, index_type());
93+
const exprt constant = from_integer(i, c_index_type());
9494

9595
const cpp_namet array(member_base_name, source_location);
9696

‎src/cpp/cpp_typecheck_conversions.cpp

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -80,9 +80,7 @@ bool cpp_typecheckt::standard_conversion_array_to_pointer(
8080
{
8181
assert(expr.type().id()==ID_array);
8282

83-
index_exprt index(
84-
expr,
85-
from_integer(0, index_type()));
83+
index_exprt index(expr, from_integer(0, c_index_type()));
8684

8785
index.set(ID_C_lvalue, true);
8886

‎src/cpp/cpp_typecheck_expr.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -256,9 +256,9 @@ void cpp_typecheckt::typecheck_expr_trinary(if_exprt &expr)
256256
{
257257
// array-to-pointer conversion
258258

259-
index_exprt index1(expr.op1(), from_integer(0, index_type()));
259+
index_exprt index1(expr.op1(), from_integer(0, c_index_type()));
260260

261-
index_exprt index2(expr.op2(), from_integer(0, index_type()));
261+
index_exprt index2(expr.op2(), from_integer(0, c_index_type()));
262262

263263
address_of_exprt addr1(index1);
264264
address_of_exprt addr2(index2);

‎src/cpp/cpp_typecheck_initializer.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -244,7 +244,7 @@ void cpp_typecheckt::zero_initializer(
244244
for(mp_integer i=0; i<size; ++i)
245245
{
246246
index_exprt index(
247-
object, from_integer(i, index_type()), array_type.subtype());
247+
object, from_integer(i, c_index_type()), array_type.subtype());
248248
zero_initializer(index, array_type.subtype(), source_location, ops);
249249
}
250250
}

‎src/goto-instrument/function.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -67,7 +67,7 @@ code_function_callt function_to_call(
6767
symbol_exprt(s_it->second.name, s_it->second.type),
6868
{typecast_exprt(
6969
address_of_exprt(
70-
index_exprt(function_id_string, from_integer(0, index_type()))),
70+
index_exprt(function_id_string, from_integer(0, c_index_type()))),
7171
to_code_type(s_it->second.type).parameters()[0].type())});
7272

7373
return call;

‎src/goto-programs/builtin_functions.cpp

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -260,7 +260,7 @@ void goto_convertt::do_scanf(
260260
const address_of_exprt rhs(
261261
index_exprt(
262262
tmp_symbol.symbol_expr(),
263-
from_integer(0, index_type())));
263+
from_integer(0, c_index_type())));
264264

265265
// now use array copy
266266
codet array_copy_statement;
@@ -274,7 +274,7 @@ void goto_convertt::do_scanf(
274274
copy(array_copy_statement, OTHER, dest);
275275
#else
276276
const index_exprt new_lhs(
277-
dereference_exprt{ptr}, from_integer(0, index_type()));
277+
dereference_exprt{ptr}, from_integer(0, c_index_type()));
278278
const side_effect_expr_nondett rhs(
279279
type->subtype(), function.source_location());
280280
code_assignt assign(new_lhs, rhs);
@@ -605,7 +605,7 @@ exprt make_va_list(const exprt &expr)
605605
while(result.type().id() == ID_array &&
606606
to_array_type(result.type()).size().is_one())
607607
{
608-
result = index_exprt{result, from_integer(0, index_type())};
608+
result = index_exprt{result, from_integer(0, c_index_type())};
609609
}
610610

611611
return result;
@@ -704,8 +704,8 @@ void goto_convertt::do_havoc_slice(
704704

705705
const symbolt &nondet_contents =
706706
new_tmp_symbol(array_type, "nondet_contents", dest, source_location, mode);
707-
const exprt &nondet_contents_expr = address_of_exprt{
708-
index_exprt{nondet_contents.symbol_expr(), from_integer(0, index_type())}};
707+
const exprt &nondet_contents_expr = address_of_exprt{index_exprt{
708+
nondet_contents.symbol_expr(), from_integer(0, c_index_type())}};
709709

710710
const exprt &arg0 =
711711
typecast_exprt::conditional_cast(arguments[0], pointer_type(empty_typet{}));

‎src/goto-programs/goto_convert_side_effect.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -214,7 +214,7 @@ void goto_convertt::remove_pre(
214214
typet constant_type;
215215

216216
if(op_type.id() == ID_pointer)
217-
constant_type = index_type();
217+
constant_type = c_index_type();
218218
else if(is_number(op_type))
219219
constant_type = op_type;
220220
else
@@ -300,7 +300,7 @@ void goto_convertt::remove_post(
300300
typet constant_type;
301301

302302
if(op_type.id() == ID_pointer)
303-
constant_type = index_type();
303+
constant_type = c_index_type();
304304
else if(is_number(op_type))
305305
constant_type = op_type;
306306
else

‎src/goto-programs/goto_instruction_code.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,7 @@ code_inputt::code_inputt(
3434
optionalt<source_locationt> location)
3535
: code_inputt{{address_of_exprt(index_exprt(
3636
string_constantt(description),
37-
from_integer(0, index_type()))),
37+
from_integer(0, c_index_type()))),
3838
std::move(expression)},
3939
std::move(location)}
4040
{
@@ -62,7 +62,7 @@ code_outputt::code_outputt(
6262
optionalt<source_locationt> location)
6363
: code_outputt{{address_of_exprt(index_exprt(
6464
string_constantt(description),
65-
from_integer(0, index_type()))),
65+
from_integer(0, c_index_type()))),
6666
std::move(expression)},
6767
std::move(location)}
6868
{

‎src/goto-programs/graphml_witness.cpp

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -109,9 +109,7 @@ std::string graphml_witnesst::convert_assign_rec(
109109
forall_operands(it, assign.rhs())
110110
{
111111
index_exprt index(
112-
assign.lhs(),
113-
from_integer(i++, index_type()),
114-
type.subtype());
112+
assign.lhs(), from_integer(i++, c_index_type()), type.subtype());
115113
if(!result.empty())
116114
result+=' ';
117115
result+=convert_assign_rec(identifier, code_assignt(index, *it));

‎src/goto-programs/rewrite_union.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -82,14 +82,14 @@ void rewrite_union(exprt &expr)
8282

8383
if(op.type().id() == ID_union_tag || op.type().id() == ID_union)
8484
{
85-
exprt offset=from_integer(0, index_type());
85+
exprt offset = from_integer(0, c_index_type());
8686
expr = make_byte_extract(op, offset, expr.type());
8787
}
8888
}
8989
else if(expr.id()==ID_union)
9090
{
9191
const union_exprt &union_expr=to_union_expr(expr);
92-
exprt offset=from_integer(0, index_type());
92+
exprt offset = from_integer(0, c_index_type());
9393
side_effect_expr_nondett nondet(expr.type(), expr.source_location());
9494
expr = make_byte_update(nondet, offset, union_expr.op());
9595
}

‎src/goto-programs/string_abstraction.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -573,7 +573,7 @@ void string_abstractiont::abstract_function_call(
573573
str_args.back().type().subtype() == abstract_type.subtype(),
574574
"argument array type differs from formal parameter pointer type");
575575

576-
index_exprt idx(str_args.back(), from_integer(0, index_type()));
576+
index_exprt idx(str_args.back(), from_integer(0, c_index_type()));
577577
// disable bounds check on that one
578578
idx.set(ID_C_bounds_check, false);
579579

‎src/goto-programs/string_instrumentation.cpp

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -394,7 +394,7 @@ void string_instrumentationt::do_format_string_read(
394394

395395
if(arg.type().id() != ID_pointer)
396396
{
397-
index_exprt index(temp, from_integer(0, index_type()));
397+
index_exprt index(temp, from_integer(0, c_index_type()));
398398
temp=address_of_exprt(index);
399399
}
400400

@@ -437,7 +437,7 @@ void string_instrumentationt::do_format_string_read(
437437

438438
if(arg.type().id() != ID_pointer)
439439
{
440-
index_exprt index(temp, from_integer(0, index_type()));
440+
index_exprt index(temp, from_integer(0, c_index_type()));
441441
temp=address_of_exprt(index);
442442
}
443443

@@ -778,9 +778,7 @@ void string_instrumentationt::do_strerror(
778778

779779
// return a pointer to some magic buffer
780780
index_exprt index(
781-
symbol_buf.symbol_expr(),
782-
from_integer(0, index_type()),
783-
char_type());
781+
symbol_buf.symbol_expr(), from_integer(0, c_index_type()), char_type());
784782

785783
address_of_exprt ptr(index);
786784

@@ -843,7 +841,7 @@ void string_instrumentationt::invalidate_buffer(
843841
else
844842
{
845843
index_exprt index(
846-
buffer, from_integer(0, index_type()), buf_type.subtype());
844+
buffer, from_integer(0, c_index_type()), buf_type.subtype());
847845
bufp=address_of_exprt(index);
848846
}
849847

‎src/goto-symex/goto_symex.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -267,7 +267,7 @@ void goto_symext::assign_string_constant(
267267
"symbol shall have value derived from char array content");
268268

269269
const address_of_exprt string_data(
270-
index_exprt(aux_symbol.symbol_expr(), from_integer(0, index_type())));
270+
index_exprt(aux_symbol.symbol_expr(), from_integer(0, c_index_type())));
271271

272272
symex_assign.assign_symbol(char_array, expr_skeletont{}, string_data, {});
273273

‎src/goto-symex/symex_clean_expr.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -45,7 +45,7 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
4545
{
4646
byte_extract_exprt be = make_byte_extract(
4747
if_expr.false_case(),
48-
from_integer(0, index_type()),
48+
from_integer(0, c_index_type()),
4949
if_expr.true_case().type());
5050

5151
if_expr.false_case().swap(be);
@@ -93,7 +93,7 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
9393
simplify(array_size.value(), ns);
9494
expr = make_byte_extract(
9595
expr,
96-
from_integer(0, index_type()),
96+
from_integer(0, c_index_type()),
9797
array_typet(char_type(), array_size.value()));
9898
}
9999

0 commit comments

Comments
 (0)