Skip to content

Commit 80a1bb5

Browse files
Petr BauchPetr Bauch
Petr Bauch
authored and
Petr Bauch
committed
Add and check type of pointees in memory analyzer
GDB does not know (the CBMC) types but the resulting symbol table requires them.
1 parent fb5eef9 commit 80a1bb5

File tree

1 file changed

+6
-2
lines changed

1 file changed

+6
-2
lines changed

src/memory-analyzer/analyze_symbol.cpp

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -232,7 +232,9 @@ exprt symbol_analyzert::get_non_char_pointer_value(
232232
}
233233
else
234234
{
235-
return it->second;
235+
const symbol_exprt typed_symbol_value = symbol_exprt{
236+
to_symbol_expr(it->second).get_identifier(), expr.type().subtype()};
237+
return typed_symbol_value;
236238
}
237239
}
238240

@@ -268,7 +270,9 @@ exprt symbol_analyzert::get_pointer_value(
268270
}
269271
else
270272
{
271-
return address_of_exprt(target_expr);
273+
const auto result_expr = address_of_exprt(target_expr);
274+
CHECK_RETURN(result_expr.type() == zero_expr.type());
275+
return result_expr;
272276
}
273277
}
274278
}

0 commit comments

Comments
 (0)