Skip to content

Commit a0883eb

Browse files
tautschnigtautschnig
authored
Merge pull request #3087 from diffblue/type-cleanup3
do not access typet::subtype() without cast
2 parents c3b78c9 + bdfe7af commit a0883eb

18 files changed

+99
-75
lines changed

‎src/analyses/goto_rw.cpp

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -616,8 +616,9 @@ void rw_range_sett::get_objects_rec(const typet &type)
616616
// TODO should recurse into various composite types
617617
if(type.id()==ID_array)
618618
{
619-
get_objects_rec(type.subtype());
620-
get_objects_rec(get_modet::READ, to_array_type(type).size());
619+
const auto &array_type = to_array_type(type);
620+
get_objects_rec(array_type.subtype());
621+
get_objects_rec(get_modet::READ, array_type.size());
621622
}
622623
}
623624

‎src/goto-instrument/thread_instrumentation.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -140,5 +140,7 @@ void mutex_init_instrumentation(goto_modelt &goto_model)
140140

141141
Forall_goto_functions(f_it, goto_model.goto_functions)
142142
mutex_init_instrumentation(
143-
goto_model.symbol_table, f_it->second.body, lock_type.subtype());
143+
goto_model.symbol_table,
144+
f_it->second.body,
145+
to_pointer_type(lock_type).subtype());
144146
}

‎src/goto-symex/auto_objects.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -57,7 +57,7 @@ void goto_symext::initialize_auto_object(
5757
else if(type.id()==ID_pointer)
5858
{
5959
const pointer_typet &pointer_type=to_pointer_type(type);
60-
const typet &subtype=ns.follow(type.subtype());
60+
const typet &subtype = ns.follow(pointer_type.subtype());
6161

6262
// we don't like function pointers and
6363
// we don't like void *
@@ -67,7 +67,7 @@ void goto_symext::initialize_auto_object(
6767
// could be NULL nondeterministically
6868

6969
address_of_exprt address_of_expr(
70-
make_auto_object(type.subtype(), state), pointer_type);
70+
make_auto_object(pointer_type.subtype(), state), pointer_type);
7171

7272
if_exprt rhs(
7373
side_effect_expr_nondett(bool_typet(), expr.source_location()),

‎src/goto-symex/goto_symex_state.cpp

Lines changed: 11 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -96,7 +96,7 @@ static bool check_renaming(const typet &type)
9696
return true;
9797
}
9898
else if(type.has_subtype())
99-
return check_renaming(type.subtype());
99+
return check_renaming(to_type_with_subtype(type).subtype());
100100

101101
return false;
102102
}
@@ -409,7 +409,7 @@ void goto_symex_statet::rename(
409409
{
410410
auto &address_of_expr = to_address_of_expr(expr);
411411
rename_address(address_of_expr.object(), ns, level);
412-
expr.type().subtype() = address_of_expr.object().type();
412+
to_pointer_type(expr.type()).subtype() = address_of_expr.object().type();
413413
}
414414
else
415415
{
@@ -645,7 +645,7 @@ void goto_symex_statet::rename_address(
645645

646646
rename_address(index_expr.array(), ns, level);
647647
PRECONDITION(index_expr.array().type().id() == ID_array);
648-
expr.type()=index_expr.array().type().subtype();
648+
expr.type() = to_array_type(index_expr.array().type()).subtype();
649649

650650
// the index is not an address
651651
rename(index_expr.index(), ns, level);
@@ -730,8 +730,9 @@ void goto_symex_statet::rename(
730730

731731
if(type.id()==ID_array)
732732
{
733-
rename(type.subtype(), irep_idt(), ns, level);
734-
rename(to_array_type(type).size(), ns, level);
733+
auto &array_type = to_array_type(type);
734+
rename(array_type.subtype(), irep_idt(), ns, level);
735+
rename(array_type.size(), ns, level);
735736
}
736737
else if(type.id()==ID_struct ||
737738
type.id()==ID_union ||
@@ -752,7 +753,7 @@ void goto_symex_statet::rename(
752753
}
753754
else if(type.id()==ID_pointer)
754755
{
755-
rename(type.subtype(), irep_idt(), ns, level);
756+
rename(to_pointer_type(type).subtype(), irep_idt(), ns, level);
756757
}
757758
else if(type.id() == ID_symbol_type)
758759
{
@@ -796,8 +797,9 @@ void goto_symex_statet::get_original_name(typet &type) const
796797

797798
if(type.id()==ID_array)
798799
{
799-
get_original_name(type.subtype());
800-
get_original_name(to_array_type(type).size());
800+
auto &array_type = to_array_type(type);
801+
get_original_name(array_type.subtype());
802+
get_original_name(array_type.size());
801803
}
802804
else if(type.id()==ID_struct ||
803805
type.id()==ID_union ||
@@ -814,7 +816,7 @@ void goto_symex_statet::get_original_name(typet &type) const
814816
}
815817
else if(type.id()==ID_pointer)
816818
{
817-
get_original_name(type.subtype());
819+
get_original_name(to_pointer_type(type).subtype());
818820
}
819821
}
820822

‎src/goto-symex/symex_builtin_functions.cpp

Lines changed: 12 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -60,9 +60,11 @@ void goto_symext::symex_allocate(
6060
const irep_idt &mode = function_symbol->mode;
6161

6262
// is the type given?
63-
if(code.type().id()==ID_pointer && code.type().subtype().id()!=ID_empty)
63+
if(
64+
code.type().id() == ID_pointer &&
65+
to_pointer_type(code.type()).subtype().id() != ID_empty)
6466
{
65-
object_type=code.type().subtype();
67+
object_type = to_pointer_type(code.type()).subtype();
6668
}
6769
else
6870
{
@@ -190,11 +192,11 @@ void goto_symext::symex_allocate(
190192

191193
if(object_type.id()==ID_array)
192194
{
193-
index_exprt index_expr(value_symbol.type.subtype());
195+
const auto &array_type = to_array_type(object_type);
196+
index_exprt index_expr(array_type.subtype());
194197
index_expr.array()=value_symbol.symbol_expr();
195198
index_expr.index()=from_integer(0, index_type());
196-
rhs=address_of_exprt(
197-
index_expr, pointer_type(value_symbol.type.subtype()));
199+
rhs = address_of_exprt(index_expr, pointer_type(array_type.subtype()));
198200
}
199201
else
200202
{
@@ -391,6 +393,8 @@ void goto_symext::symex_cpp_new(
391393

392394
PRECONDITION(code.type().id() == ID_pointer);
393395

396+
const auto &pointer_type = to_pointer_type(code.type());
397+
394398
do_array =
395399
(code.get(ID_statement) == ID_cpp_new_array ||
396400
code.get(ID_statement) == ID_java_new_array_data);
@@ -418,19 +422,18 @@ void goto_symext::symex_cpp_new(
418422
{
419423
exprt size_arg = static_cast<const exprt &>(code.find(ID_size));
420424
clean_expr(size_arg, state, false);
421-
symbol.type = array_typet(code.type().subtype(), size_arg);
425+
symbol.type = array_typet(pointer_type.subtype(), size_arg);
422426
}
423427
else
424-
symbol.type=code.type().subtype();
428+
symbol.type = pointer_type.subtype();
425429

426430
symbol.type.set(ID_C_dynamic, true);
427431

428432
state.symbol_table.add(symbol);
429433

430434
// make symbol expression
431435

432-
exprt rhs(ID_address_of, code.type());
433-
rhs.type().subtype()=code.type().subtype();
436+
exprt rhs(ID_address_of, pointer_type);
434437

435438
if(do_array)
436439
{

‎src/goto-symex/symex_dereference.cpp

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -338,8 +338,11 @@ void goto_symext::dereference_rec(
338338
exprt &object=address_of_expr.object();
339339

340340
const typet &expr_type=ns.follow(expr.type());
341-
expr=address_arithmetic(object, state, guard,
342-
expr_type.subtype().id()==ID_array);
341+
expr = address_arithmetic(
342+
object,
343+
state,
344+
guard,
345+
to_pointer_type(expr_type).subtype().id() == ID_array);
343346
}
344347
else if(expr.id()==ID_typecast)
345348
{

‎src/util/arith_tools.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -72,7 +72,7 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)
7272
}
7373
else if(type_id==ID_c_bit_field)
7474
{
75-
const typet &subtype=type.subtype();
75+
const typet &subtype = to_c_bit_field_type(type).subtype();
7676
if(subtype.id()==ID_signedbv)
7777
{
7878
int_value = bv2integer(id2string(value), true);

‎src/util/expr_initializer.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -116,7 +116,8 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
116116
result = side_effect_expr_nondett(type, source_location);
117117
else
118118
{
119-
exprt sub_zero = expr_initializer_rec(type.subtype(), source_location);
119+
exprt sub_zero =
120+
expr_initializer_rec(to_complex_type(type).subtype(), source_location);
120121
result = complex_exprt(sub_zero, sub_zero, to_complex_type(type));
121122
}
122123

‎src/util/find_symbols.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -124,7 +124,7 @@ void find_symbols(kindt kind, const typet &src, find_symbols_sett &dest)
124124
src.id()!=ID_pointer)
125125
{
126126
if(src.has_subtype())
127-
find_symbols(kind, src.subtype(), dest);
127+
find_symbols(kind, to_type_with_subtype(src).subtype(), dest);
128128

129129
forall_subtypes(it, src)
130130
find_symbols(kind, *it, dest);

‎src/util/format_type.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -60,14 +60,14 @@ std::ostream &format_rec(std::ostream &os, const typet &type)
6060
const auto &id = type.id();
6161

6262
if(id == ID_pointer)
63-
return os << '*' << format(type.subtype());
63+
return os << '*' << format(to_pointer_type(type).subtype());
6464
else if(id == ID_array)
6565
{
6666
const auto &t = to_array_type(type);
6767
if(t.is_complete())
68-
return os << format(type.subtype()) << '[' << format(t.size()) << ']';
68+
return os << format(t.subtype()) << '[' << format(t.size()) << ']';
6969
else
70-
return os << format(type.subtype()) << "[]";
70+
return os << format(t.subtype()) << "[]";
7171
}
7272
else if(id == ID_struct)
7373
return format_rec(os, to_struct_type(type));

0 commit comments

Comments
 (0)