Skip to content

Commit

Permalink
Make get_array return array of unknown expr
Browse files Browse the repository at this point in the history
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
  • Loading branch information
romainbrenguier committed Oct 28, 2017
1 parent ca8213f commit 4b8a421
Showing 1 changed file with 10 additions and 0 deletions.
10 changes: 10 additions & 0 deletions src/solvers/refinement/string_refinement.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -733,6 +733,16 @@ static optionalt<exprt> get_array(
ret.move_to_operands(arr_val.operands()[i]);
return ret;
}
else if(arr_val.id() == ID_symbol)
{
stream << "(sr::get_array) warning: symbol "
<< to_symbol_expr(arr_val).get_identifier()
<< " not found by super_get" << eom;
// `super_get` does not know anything about this array so we make one up
for(size_t i = 0; i < n; i++)
ret.copy_to_operands(exprt(ID_unknown, arr_val.type().subtype()));
return ret;
}
else
return {};
}
Expand Down

0 comments on commit 4b8a421

Please sign in to comment.