From 08a71e928476ad2ea15ffd87f59f2147369baa9b Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 6 Aug 2019 07:32:20 +0100 Subject: [PATCH] Attempt to get missing array size from symbol table In some cases, like the test in regression/cbmc/Global_Initialization2, the array type is incomplete and changed in the symbol table after the main function has been converted, leading to inconsistencies. This means we can get nil instead of the size in field_sensitivityt::apply, though the actual size is present in the symbol table. The issue is reported here: https://github.com/diffblue/cbmc/issues/5022 --- src/goto-symex/field_sensitivity.cpp | 19 ++++++++++++++++--- 1 file changed, 16 insertions(+), 3 deletions(-) diff --git a/src/goto-symex/field_sensitivity.cpp b/src/goto-symex/field_sensitivity.cpp index a08af7810e..3cf6f7ab87 100644 --- a/src/goto-symex/field_sensitivity.cpp +++ b/src/goto-symex/field_sensitivity.cpp @@ -97,10 +97,23 @@ exprt field_sensitivityt::apply( // SSA expression ssa_exprt tmp = to_ssa_expr(index.array()); bool was_l2 = !tmp.get_level_2().empty(); + + exprt array_size_expr = to_array_type(l2_array.get().type()).size(); + if(array_size_expr.is_nil() && index.array().id() == ID_symbol) + { + // In case the array type was incomplete, attempt to retrieve it from + // the symbol table. + const symbolt *array_from_symbol_table = ns.get_symbol_table().lookup( + to_symbol_expr(index.array()).get_identifier()); + if(array_from_symbol_table != nullptr) + array_size_expr = to_array_type(array_from_symbol_table->type).size(); + } + if( - l2_size.id() == ID_constant && - numeric_cast_v(to_constant_expr(l2_size)) <= - MAX_FIELD_SENSITIVITY_ARRAY_SIZE) + array_size_expr.id() == ID_constant && + numeric_cast_v(to_constant_expr(array_size_expr)) <= + MAX_FIELD_SENSITIVITY_ARRAY_SIZE && + index.id() == ID_constant) { tmp.remove_level_2(); index.array() = tmp.get_original_expr();