Skip to content

Commit

Permalink
Use numeric_cast instead of other conversion
Browse files Browse the repository at this point in the history
This is to demonstrate the use of numeric_cast
  • Loading branch information
romainbrenguier committed Dec 8, 2017
1 parent fc294f8 commit 5683fb5
Showing 1 changed file with 9 additions and 7 deletions.
16 changes: 9 additions & 7 deletions src/solvers/refinement/string_refinement.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -794,12 +794,13 @@ static optionalt<exprt> get_array(
return {};
}

unsigned n;
if(to_unsigned_integer(to_constant_expr(size_val), n))
auto n_opt = numeric_cast<unsigned>(size_val);
if(!n_opt)
{
stream << "(sr::get_array) size is not valid" << eom;
return {};
}
unsigned n = *n_opt;

const array_typet ret_type(char_type, from_integer(n, index_type));
array_exprt ret(ret_type);
Expand All @@ -824,9 +825,11 @@ static optionalt<exprt> get_array(
for(size_t i = 0; i < arr_val.operands().size(); i += 2)
{
exprt index = arr_val.operands()[i];
unsigned idx;
if(!to_unsigned_integer(to_constant_expr(index), idx) && idx<n)
initial_map[idx] = arr_val.operands()[i + 1];
if(auto idx = numeric_cast<std::size_t>(index))
{
if(*idx < n)
initial_map[*idx] = arr_val.operands()[i + 1];
}
}

// Pad the concretized values to the left to assign the uninitialized
Expand Down Expand Up @@ -855,8 +858,7 @@ static std::string string_of_array(const array_exprt &arr)
return std::string("");

exprt size_expr=to_array_type(arr.type()).size();
PRECONDITION(size_expr.id()==ID_constant);
to_unsigned_integer(to_constant_expr(size_expr), n);
auto n = numeric_cast_v<unsigned>(size_expr);
return utf16_constant_array_to_java(arr, n);
}

Expand Down

0 comments on commit 5683fb5

Please sign in to comment.