Skip to content

Commit 4b8a421

Browse files
Make get_array return array of unknown expr
This is in the case where super_get does not anything about the array we give it. This is necessary so that the string solver returns an array of the correct size, if the size is the only thing we know about the string. Add warning message in the case where the symbol is unknown to super_get
1 parent ca8213f commit 4b8a421

File tree

1 file changed

+10
-0
lines changed

1 file changed

+10
-0
lines changed

src/solvers/refinement/string_refinement.cpp

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -733,6 +733,16 @@ static optionalt<exprt> get_array(
733733
ret.move_to_operands(arr_val.operands()[i]);
734734
return ret;
735735
}
736+
else if(arr_val.id() == ID_symbol)
737+
{
738+
stream << "(sr::get_array) warning: symbol "
739+
<< to_symbol_expr(arr_val).get_identifier()
740+
<< " not found by super_get" << eom;
741+
// `super_get` does not know anything about this array so we make one up
742+
for(size_t i = 0; i < n; i++)
743+
ret.copy_to_operands(exprt(ID_unknown, arr_val.type().subtype()));
744+
return ret;
745+
}
736746
else
737747
return {};
738748
}

0 commit comments

Comments
 (0)