replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

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
This commit is contained in:
Romain Brenguier 2019-08-06 07:32:20 +01:00
parent 7b958bf4c9
commit 08a71e9284
1 changed files with 16 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
src/goto-symex/field_sensitivity.cpp
View File

@ -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<mp_integer>(to_constant_expr(l2_size)) <=
MAX_FIELD_SENSITIVITY_ARRAY_SIZE)
array_size_expr.id() == ID_constant &&
numeric_cast_v<mp_integer>(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();