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

Construct array_list_exprt in a non-deprecated way 

The existing array_list_exprt constructor relies on other deprecated
constructors; instead introduce a non-deprecated one and use it across the
codebase.
This commit is contained in:
Michael Tautschnig 2019-01-12 18:21:45 +00:00
parent 80cb920a68
commit 1ae4c0ba62
3 changed files with 9 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/solvers/flattening/boolbv_get.cpp
View File

@ -361,7 +361,7 @@ exprt boolbvt::bv_get_unbounded_array(const exprt &expr) const
if(size_mpint>100 || size.id()==ID_infinity)
{
result = array_list_exprt(to_array_type(type));
result = array_list_exprt({}, to_array_type(type));
result.type().set(ID_size, integer2string(size_mpint));
result.operands().reserve(values.size()*2);

5
src/util/std_expr.h
View File

@ -1796,6 +1796,11 @@ public:
: multi_ary_exprt(ID_array_list, _type)
{
}
array_list_exprt(operandst &&_operands, const array_typet &_type)
: multi_ary_exprt(ID_array_list, std::move(_operands), _type)
{
}
};
template <>

6
unit/solvers/refinement/string_refinement/substitute_array_list.cpp
View File

@ -21,7 +21,6 @@ SCENARIO("substitute_array_list",
const typet char_type=unsignedbv_typet(16);
const typet int_type=signedbv_typet(32);
const array_typet array_type(char_type, infinity_exprt(int_type));
array_list_exprt arr(array_type);
const exprt index0=from_integer(0, int_type);
const exprt charx=from_integer('x', char_type);
const exprt index1=from_integer(1, int_type);
@ -29,8 +28,9 @@ SCENARIO("substitute_array_list",
const exprt index100=from_integer(100, int_type);
// arr is `array-list [ 0 , 'x' , 1 , 'y' , 2 , 'z']`
arr.operands()=
{ index0, charx, index1, chary, index100, from_integer('z', char_type) };
array_list_exprt arr(
{index0, charx, index1, chary, index100, from_integer('z', char_type)},
array_type);
// Max length is 2, so index 2 should get ignored.
const exprt subst=substitute_array_lists(arr, 2);