Skip to content

Commit dbc301f

Browse files
authored
Merge pull request #3647 from diffblue/symbol_factoryt_fix
bugfix: symbol_factoryt must preserve struct_tag types [blocks: #3652]
2 parents c2b1573 + b552cc1 commit dbc301f

File tree

1 file changed

+9
-8
lines changed

1 file changed

+9
-8
lines changed

src/ansi-c/c_nondet_symbol_factory.cpp

+9-8
Original file line numberDiff line numberDiff line change
@@ -96,18 +96,17 @@ void symbol_factoryt::gen_nondet_init(
9696
const std::size_t depth,
9797
recursion_sett recursion_set)
9898
{
99-
const typet &type=ns.follow(expr.type());
99+
const typet &type = expr.type();
100100

101101
if(type.id()==ID_pointer)
102102
{
103103
// dereferenced type
104104
const pointer_typet &pointer_type=to_pointer_type(type);
105-
const typet &subtype=ns.follow(pointer_type.subtype());
105+
const typet &subtype = pointer_type.subtype();
106106

107-
if(subtype.id() == ID_struct)
107+
if(subtype.id() == ID_struct_tag)
108108
{
109-
const struct_typet &struct_type = to_struct_type(subtype);
110-
const irep_idt struct_tag = struct_type.get_tag();
109+
const irep_idt struct_tag = to_struct_tag_type(subtype).get_identifier();
111110

112111
if(
113112
recursion_set.find(struct_tag) != recursion_set.end() &&
@@ -153,14 +152,16 @@ void symbol_factoryt::gen_nondet_init(
153152
assignments.add(std::move(null_check));
154153
}
155154
}
156-
else if(type.id() == ID_struct)
155+
else if(type.id() == ID_struct_tag)
157156
{
158-
const struct_typet &struct_type = to_struct_type(type);
157+
const auto &struct_tag_type = to_struct_tag_type(type);
159158

160-
const irep_idt struct_tag = struct_type.get_tag();
159+
const irep_idt struct_tag = struct_tag_type.get_identifier();
161160

162161
recursion_set.insert(struct_tag);
163162

163+
const auto &struct_type = to_struct_type(ns.follow_tag(struct_tag_type));
164+
164165
for(const auto &component : struct_type.components())
165166
{
166167
const typet &component_type = component.type();

0 commit comments

Comments
 (0)