Skip to content

Commit d26743a

Browse files
committed
Use conditional_cast instead of make_type
No need for a local helper that unnecessarily used `follow`.
1 parent d7b229e commit d26743a

File tree

3 files changed

+13
-30
lines changed

3 files changed

+13
-30
lines changed

src/goto-programs/string_abstraction.cpp

+12-15
Original file line numberDiff line numberDiff line change
@@ -442,10 +442,9 @@ symbol_exprt string_abstractiont::add_dummy_symbol_and_value(
442442
build_unknown(whatt::LENGTH, false),
443443
to_array_type(source_type).size().id() == ID_infinity
444444
? build_unknown(whatt::SIZE, false)
445-
: to_array_type(source_type).size()},
445+
: typecast_exprt::conditional_cast(
446+
to_array_type(source_type).size(), build_type(whatt::SIZE))},
446447
string_struct);
447-
448-
make_type(to_struct_expr(new_symbol.value).op2(), build_type(whatt::SIZE));
449448
}
450449
else
451450
new_symbol.value=
@@ -1212,8 +1211,8 @@ goto_programt::targett string_abstractiont::abstract_char_assign(
12121211
i2.is_not_nil(),
12131212
"failed to create length-component for the left-hand-side");
12141213

1215-
exprt new_length=i_lhs.index();
1216-
make_type(new_length, i2.type());
1214+
exprt new_length =
1215+
typecast_exprt::conditional_cast(i_lhs.index(), i2.type());
12171216

12181217
if_exprt min_expr(binary_relation_exprt(new_length, ID_lt, i2),
12191218
new_length, i2);
@@ -1232,16 +1231,14 @@ goto_programt::targett string_abstractiont::abstract_char_assign(
12321231
i2.is_not_nil(),
12331232
"failed to create length-component for the left-hand-side");
12341233

1235-
make_type(ptr.offset, build_type(whatt::LENGTH));
1236-
return
1237-
char_assign(
1238-
dest,
1239-
target,
1240-
new_lhs,
1241-
i2,
1242-
ptr.offset.is_nil()?
1243-
from_integer(0, build_type(whatt::LENGTH)):
1244-
ptr.offset);
1234+
return char_assign(
1235+
dest,
1236+
target,
1237+
new_lhs,
1238+
i2,
1239+
ptr.offset.is_nil() ? from_integer(0, build_type(whatt::LENGTH))
1240+
: typecast_exprt::conditional_cast(
1241+
ptr.offset, build_type(whatt::LENGTH)));
12451242
}
12461243
}
12471244

src/goto-programs/string_abstraction.h

-7
Original file line numberDiff line numberDiff line change
@@ -73,13 +73,6 @@ class string_abstractiont
7373

7474
bool is_ptr_string_struct(const typet &type) const;
7575

76-
void make_type(exprt &dest, const typet &type)
77-
{
78-
if(dest.is_not_nil() &&
79-
ns.follow(dest.type())!=ns.follow(type))
80-
dest = typecast_exprt(dest, type);
81-
}
82-
8376
goto_programt::targett abstract(
8477
goto_programt &dest, goto_programt::targett it);
8578
goto_programt::targett abstract_assign(

src/goto-programs/string_instrumentation.cpp

+1-8
Original file line numberDiff line numberDiff line change
@@ -64,12 +64,6 @@ class string_instrumentationt
6464
symbol_table_baset &symbol_table;
6565
namespacet ns;
6666

67-
void make_type(exprt &dest, const typet &type)
68-
{
69-
if(ns.follow(dest.type())!=ns.follow(type))
70-
dest = typecast_exprt(dest, type);
71-
}
72-
7367
void instrument(goto_programt &dest, goto_programt::targett it);
7468
void do_function_call(goto_programt &dest, goto_programt::targett target);
7569

@@ -785,8 +779,7 @@ void string_instrumentationt::do_strerror(
785779

786780
// assign address
787781
{
788-
exprt rhs=ptr;
789-
make_type(rhs, lhs.type());
782+
exprt rhs = typecast_exprt::conditional_cast(ptr, lhs.type());
790783
tmp.add(goto_programt::make_assignment(
791784
code_assignt(lhs, rhs), it->source_location()));
792785
}

0 commit comments

Comments
 (0)