Skip to content

Commit

Permalink
goto-programs: Replace uses of namespacet::follow
Browse files Browse the repository at this point in the history
This is deprecated. Use suitable variants of `follow_tag` instead.
  • Loading branch information
tautschnig committed Mar 6, 2024
1 parent 3b76fc8 commit b1d1ccf
Show file tree
Hide file tree
Showing 10 changed files with 81 additions and 73 deletions.
7 changes: 4 additions & 3 deletions src/goto-programs/class_identifier.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -28,8 +28,8 @@ static exprt build_class_identifier(

while(1)
{
const typet &type=ns.follow(e.type());
const struct_typet &struct_type=to_struct_type(type);
const struct_typet &struct_type =
ns.follow_tag(to_struct_tag_type(e.type()));
const struct_typet::componentst &components=struct_type.components();
INVARIANT(!components.empty(), "class structs cannot be empty");

Expand Down Expand Up @@ -85,7 +85,8 @@ void set_class_identifier(
const namespacet &ns,
const struct_tag_typet &class_type)
{
const struct_typet &struct_type=to_struct_type(ns.follow(expr.type()));
const struct_typet &struct_type =
ns.follow_tag(to_struct_tag_type(expr.type()));
const struct_typet::componentst &components=struct_type.components();

if(components.empty())
Expand Down
8 changes: 6 additions & 2 deletions src/goto-programs/destructor.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -38,9 +38,13 @@ code_function_callt get_destructor(
{
const typet &arg_type=code_type.parameters().front().type();

if(arg_type.id() != ID_pointer)
continue;

Check warning on line 42 in src/goto-programs/destructor.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/destructor.cpp#L42

Added line #L42 was not covered by tests

const typet &base_type = to_pointer_type(arg_type).base_type();
if(
arg_type.id() == ID_pointer &&
ns.follow(to_pointer_type(arg_type).base_type()) == type)
base_type.id() == ID_struct_tag &&
ns.follow_tag(to_struct_tag_type(base_type)) == type)
{
const symbol_exprt symbol_expr(op.get(ID_name), op.type());
return code_function_callt(symbol_expr);
Expand Down
11 changes: 7 additions & 4 deletions src/goto-programs/graphml_witness.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -132,10 +132,13 @@ std::string graphml_witnesst::convert_assign_rec(
return convert_assign_rec(identifier, tmp);
}

const struct_union_typet &type=
to_struct_union_type(ns.follow(assign.lhs().type()));
const struct_union_typet::componentst &components=
type.components();
const typet &lhs_type = assign.lhs().type();
const struct_union_typet::componentst &components =
lhs_type.id() == ID_struct_tag
? ns.follow_tag(to_struct_tag_type(lhs_type)).components()
: lhs_type.id() == ID_union_tag
? ns.follow_tag(to_union_tag_type(lhs_type)).components()
: to_struct_union_type(lhs_type).components();

Check warning on line 141 in src/goto-programs/graphml_witness.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/graphml_witness.cpp#L135-L141

Added lines #L135 - L141 were not covered by tests

exprt::operandst::const_iterator it=
assign.rhs().operands().begin();
Expand Down
44 changes: 21 additions & 23 deletions src/goto-programs/interpreter.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -424,11 +424,11 @@ void interpretert::execute_decl()
struct_typet::componentt
interpretert::get_component(const typet &object_type, const mp_integer &offset)
{
const typet real_type = ns.follow(object_type);
if(real_type.id()!=ID_struct)
if(object_type.id() != ID_struct_tag)

Check warning on line 427 in src/goto-programs/interpreter.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/interpreter.cpp#L427

Added line #L427 was not covered by tests
throw "request for member of non-struct";

const struct_typet &struct_type=to_struct_type(real_type);
const struct_typet &struct_type =
ns.follow_tag(to_struct_tag_type(object_type));

Check warning on line 431 in src/goto-programs/interpreter.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/interpreter.cpp#L430-L431

Added lines #L430 - L431 were not covered by tests
const struct_typet::componentst &components=struct_type.components();

mp_integer tmp_offset=offset;
Expand Down Expand Up @@ -460,11 +460,10 @@ exprt interpretert::get_value(
const mp_integer &offset,
bool use_non_det)
{
const typet real_type=ns.follow(type);
if(real_type.id()==ID_struct)
if(type.id() == ID_struct_tag)

Check warning on line 463 in src/goto-programs/interpreter.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/interpreter.cpp#L463

Added line #L463 was not covered by tests
{
struct_exprt result({}, real_type);
const struct_typet &struct_type=to_struct_type(real_type);
struct_exprt result({}, type);
const struct_typet &struct_type = ns.follow_tag(to_struct_tag_type(type));

Check warning on line 466 in src/goto-programs/interpreter.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/interpreter.cpp#L465-L466

Added lines #L465 - L466 were not covered by tests
const struct_typet::componentst &components=struct_type.components();

// Retrieve the values for the individual members
Expand All @@ -482,10 +481,10 @@ exprt interpretert::get_value(

return std::move(result);
}
else if(real_type.id()==ID_array)
else if(type.id() == ID_array)

Check warning on line 484 in src/goto-programs/interpreter.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/interpreter.cpp#L484

Added line #L484 was not covered by tests
{
// Get size of array
array_exprt result({}, to_array_type(real_type));
array_exprt result({}, to_array_type(type));

Check warning on line 487 in src/goto-programs/interpreter.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/interpreter.cpp#L487

Added line #L487 was not covered by tests
const exprt &size_expr = to_array_type(type).size();
mp_integer subtype_size = get_size(to_array_type(type).element_type());
mp_integer count;
Expand Down Expand Up @@ -526,13 +525,12 @@ exprt interpretert::get_value(
mp_vectort &rhs,
const mp_integer &offset)
{
const typet real_type=ns.follow(type);
PRECONDITION(!rhs.empty());

if(real_type.id()==ID_struct)
if(type.id() == ID_struct_tag)
{
struct_exprt result({}, real_type);
const struct_typet &struct_type=to_struct_type(real_type);
struct_exprt result({}, type);
const struct_typet &struct_type = ns.follow_tag(to_struct_tag_type(type));

Check warning on line 533 in src/goto-programs/interpreter.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/interpreter.cpp#L532-L533

Added lines #L532 - L533 were not covered by tests
const struct_typet::componentst &components=struct_type.components();

// Retrieve the values for the individual members
Expand All @@ -548,10 +546,10 @@ exprt interpretert::get_value(
}
return std::move(result);
}
else if(real_type.id()==ID_array)
else if(type.id() == ID_array)
{
array_exprt result({}, to_array_type(real_type));
const exprt &size_expr = to_array_type(real_type).size();
array_exprt result({}, to_array_type(type));
const exprt &size_expr = to_array_type(type).size();

Check warning on line 552 in src/goto-programs/interpreter.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/interpreter.cpp#L551-L552

Added lines #L551 - L552 were not covered by tests

// Get size of array
mp_integer subtype_size = get_size(to_array_type(type).element_type());
Expand All @@ -576,34 +574,34 @@ exprt interpretert::get_value(
}
return std::move(result);
}
else if(real_type.id()==ID_floatbv)
else if(type.id() == ID_floatbv)
{
ieee_floatt f(to_floatbv_type(type));
f.unpack(rhs[numeric_cast_v<std::size_t>(offset)]);
return f.to_expr();
}
else if(real_type.id()==ID_fixedbv)
else if(type.id() == ID_fixedbv)
{
fixedbvt f;
f.from_integer(rhs[numeric_cast_v<std::size_t>(offset)]);
return f.to_expr();
}
else if(real_type.id()==ID_bool)
else if(type.id() == ID_bool)
{
if(rhs[numeric_cast_v<std::size_t>(offset)] != 0)
return true_exprt();
else
false_exprt();
}
else if(real_type.id()==ID_c_bool)
else if(type.id() == ID_c_bool)
{
return from_integer(
rhs[numeric_cast_v<std::size_t>(offset)] != 0 ? 1 : 0, type);
}
else if(real_type.id() == ID_pointer)
else if(type.id() == ID_pointer)
{
if(rhs[numeric_cast_v<std::size_t>(offset)] == 0)
return null_pointer_exprt(to_pointer_type(real_type)); // NULL pointer
return null_pointer_exprt(to_pointer_type(type)); // NULL pointer

if(rhs[numeric_cast_v<std::size_t>(offset)] < memory.size())
{
Expand Down Expand Up @@ -634,7 +632,7 @@ exprt interpretert::get_value(

throw "interpreter: reading from invalid pointer";
}
else if(real_type.id()==ID_string)
else if(type.id() == ID_string)
{
// Strings are currently encoded by their irep_idt ID.
return constant_exprt(
Expand Down
2 changes: 1 addition & 1 deletion src/goto-programs/interpreter_evaluate.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1042,7 +1042,7 @@ mp_integer interpretert::evaluate_address(
else if(expr.id()==ID_member)
{
const struct_typet &struct_type =
to_struct_type(ns.follow(to_member_expr(expr).compound().type()));
ns.follow_tag(to_struct_tag_type(to_member_expr(expr).compound().type()));

Check warning on line 1045 in src/goto-programs/interpreter_evaluate.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/interpreter_evaluate.cpp#L1045

Added line #L1045 was not covered by tests

const irep_idt &component_name=
to_member_expr(expr).get_component_name();
Expand Down
30 changes: 14 additions & 16 deletions src/goto-programs/json_expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -361,24 +361,22 @@ json_objectt json(const exprt &expr, const namespacet &ns, const irep_idt &mode)
{
result["name"] = json_stringt("struct");

const typet &type = ns.follow(expr.type());
const struct_typet &struct_type =
expr.type().id() == ID_struct_tag
? ns.follow_tag(to_struct_tag_type(expr.type()))
: to_struct_type(expr.type());

Check warning on line 367 in src/goto-programs/json_expr.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/json_expr.cpp#L367

Added line #L367 was not covered by tests
const struct_typet::componentst &components = struct_type.components();
DATA_INVARIANT(
components.size() == expr.operands().size(),
"number of struct components should match with its type");

// these are expected to have a struct type
if(type.id() == ID_struct)
json_arrayt &members = result["members"].make_array();
for(std::size_t m = 0; m < expr.operands().size(); m++)
{
const struct_typet &struct_type = to_struct_type(type);
const struct_typet::componentst &components = struct_type.components();
DATA_INVARIANT(
components.size() == expr.operands().size(),
"number of struct components should match with its type");

json_arrayt &members = result["members"].make_array();
for(std::size_t m = 0; m < expr.operands().size(); m++)
{
json_objectt e{{"value", json(expr.operands()[m], ns, mode)},
{"name", json_stringt(components[m].get_name())}};
members.push_back(std::move(e));
}
json_objectt e{
{"value", json(expr.operands()[m], ns, mode)},
{"name", json_stringt(components[m].get_name())}};
members.push_back(std::move(e));
}
}
else if(expr.id() == ID_union)
Expand Down
3 changes: 2 additions & 1 deletion src/goto-programs/remove_const_function_pointers.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -800,7 +800,8 @@ bool remove_const_function_pointerst::is_const_type(const typet &type) const
exprt remove_const_function_pointerst::get_component_value(
const struct_exprt &struct_expr, const member_exprt &member_expr)
{
const struct_typet &struct_type=to_struct_type(ns.follow(struct_expr.type()));
const struct_typet &struct_type =
ns.follow_tag(to_struct_tag_type(struct_expr.type()));
size_t component_number=
struct_type.component_number(member_expr.get_component_name());

Expand Down
5 changes: 4 additions & 1 deletion src/goto-programs/rewrite_union.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -139,7 +139,10 @@ static bool restore_union_rec(exprt &expr, const namespacet &ns)
byte_extract_exprt &be = to_byte_extract_expr(expr);
if(be.op().type().id() == ID_union || be.op().type().id() == ID_union_tag)
{
const union_typet &union_type = to_union_type(ns.follow(be.op().type()));
const union_typet &union_type =
be.op().type().id() == ID_union_tag
? ns.follow_tag(to_union_tag_type(be.op().type()))
: to_union_type(be.op().type());

for(const auto &comp : union_type.components())
{
Expand Down
21 changes: 12 additions & 9 deletions src/goto-programs/string_abstraction.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -353,14 +353,14 @@ exprt string_abstractiont::make_val_or_dummy_rec(goto_programt &dest,
symbol.type.id() == ID_union_tag ||
(symbol.type.id() == ID_struct_tag && symbol.type != string_struct))
{
const struct_union_typet &su_source =
to_struct_union_type(ns.follow(source_type));
const struct_union_typet::componentst &s_components=
su_source.components();
const struct_union_typet &struct_union_type =
to_struct_union_type(ns.follow(symbol.type));
const struct_union_typet::componentst &components=
struct_union_type.components();
const struct_union_typet::componentst &s_components =
source_type.id() == ID_struct_tag
? ns.follow_tag(to_struct_tag_type(source_type)).components()
: ns.follow_tag(to_union_tag_type(source_type)).components();

Check warning on line 359 in src/goto-programs/string_abstraction.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/string_abstraction.cpp#L359

Added line #L359 was not covered by tests
const struct_union_typet::componentst &components =
symbol.type.id() == ID_struct_tag
? ns.follow_tag(to_struct_tag_type(symbol.type)).components()
: ns.follow_tag(to_union_tag_type(symbol.type)).components();

Check warning on line 363 in src/goto-programs/string_abstraction.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/string_abstraction.cpp#L363

Added line #L363 was not covered by tests
unsigned seen=0;

struct_union_typet::componentst::const_iterator it2=components.begin();
Expand Down Expand Up @@ -732,7 +732,10 @@ const typet &string_abstractiont::build_abstraction_type_rec(const typet &type,
else if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
{
const struct_union_typet &struct_union_type =
to_struct_union_type(ns.follow(type));
type.id() == ID_struct_tag ? static_cast<const struct_union_typet &>(
ns.follow_tag(to_struct_tag_type(type)))
: static_cast<const struct_union_typet &>(
ns.follow_tag(to_union_tag_type(type)));

struct_union_typet::componentst new_comp;
for(const auto &comp : struct_union_type.components())
Expand Down
23 changes: 10 additions & 13 deletions src/goto-programs/xml_expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -253,21 +253,18 @@ xmlt xml(const exprt &expr, const namespacet &ns)
{
result.name = "struct";

const typet &type = ns.follow(expr.type());
const struct_typet &struct_type =
expr.type().id() == ID_struct_tag
? ns.follow_tag(to_struct_tag_type(expr.type()))
: to_struct_type(expr.type());

Check warning on line 259 in src/goto-programs/xml_expr.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-programs/xml_expr.cpp#L259

Added line #L259 was not covered by tests
const struct_typet::componentst &components = struct_type.components();
PRECONDITION(components.size() == expr.operands().size());

// these are expected to have a struct type
if(type.id() == ID_struct)
for(unsigned m = 0; m < expr.operands().size(); m++)
{
const struct_typet &struct_type = to_struct_type(type);
const struct_typet::componentst &components = struct_type.components();
PRECONDITION(components.size() == expr.operands().size());

for(unsigned m = 0; m < expr.operands().size(); m++)
{
xmlt &e = result.new_element("member");
e.new_element() = xml(expr.operands()[m], ns);
e.set_attribute("name", id2string(components[m].get_name()));
}
xmlt &e = result.new_element("member");
e.new_element() = xml(expr.operands()[m], ns);
e.set_attribute("name", id2string(components[m].get_name()));
}
}
else if(expr.id() == ID_union)
Expand Down

0 comments on commit b1d1ccf

Please sign in to comment.