Skip to content

Commit 73d258c

Browse files
tautschnigkroening
authored andcommitted
Fix type inconsistencies in variable sensitivity
Abstract struct predicates have members with component type, not struct type. Unit tests: concrete arrays over signedbv(32) have a subtype that's signedbv(32).
1 parent 3c4e26c commit 73d258c

File tree

2 files changed

+4
-3
lines changed

2 files changed

+4
-3
lines changed

src/analyses/variable-sensitivity/full_struct_abstract_object.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -305,11 +305,13 @@ abstract_object_pointert full_struct_abstract_objectt::visit_sub_elements(
305305
exprt full_struct_abstract_objectt::to_predicate_internal(
306306
const exprt &name) const
307307
{
308+
const auto &compound_type = to_struct_union_type(name.type());
308309
auto all_predicates = exprt::operandst{};
309310

310311
for(auto field : map.get_sorted_view())
311312
{
312-
auto field_name = member_exprt(name, field.first, name.type());
313+
auto field_name =
314+
member_exprt(name, compound_type.get_component(field.first));
313315
auto field_expr = field.second->to_predicate(field_name);
314316

315317
if(!field_expr.is_true())

unit/analyses/variable-sensitivity/full_array_abstract_object/array_builder.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -29,8 +29,7 @@ full_array_abstract_objectt::full_array_pointert build_array(
2929
{
3030
const typet type = signedbv_typet(32);
3131

32-
const array_typet array_type(
33-
integer_typet(), from_integer(array.size(), type));
32+
const array_typet array_type(type, from_integer(array.size(), type));
3433

3534
exprt::operandst element_ops;
3635

0 commit comments

Comments
 (0)