Merge pull request #3775 from tautschnig/deprecation-struct_exprt
Construct struct_exprt in a non-deprecated way
This commit is contained in:
commit
4022dfbc3a
|
@ -836,14 +836,11 @@ codet java_string_library_preprocesst::code_assign_components_to_java_string(
|
|||
// A String has a field Object with @clsid = String
|
||||
const symbolt &jlo_symbol = *symbol_table.lookup("java::java.lang.Object");
|
||||
const struct_typet &jlo_struct = to_struct_type(jlo_symbol.type);
|
||||
struct_exprt jlo_init(jlo_struct);
|
||||
struct_exprt jlo_init({}, jlo_struct);
|
||||
irep_idt clsid = get_tag(lhs.type().subtype());
|
||||
java_root_class_init(jlo_init, jlo_struct, clsid);
|
||||
|
||||
struct_exprt struct_rhs(deref.type());
|
||||
struct_rhs.copy_to_operands(jlo_init);
|
||||
struct_rhs.copy_to_operands(rhs_length);
|
||||
struct_rhs.copy_to_operands(rhs_array);
|
||||
struct_exprt struct_rhs({jlo_init, rhs_length, rhs_array}, deref.type());
|
||||
return code_assignt(
|
||||
checked_dereference(lhs, lhs.type().subtype()), struct_rhs);
|
||||
}
|
||||
|
@ -1342,7 +1339,7 @@ struct_exprt java_string_library_preprocesst::make_argument_for_format(
|
|||
{
|
||||
// Declarations of the fields of arg_i_struct
|
||||
// arg_i_struct is { arg_i_string_expr, tmp_int, tmp_char, ... }
|
||||
struct_exprt arg_i_struct(structured_type);
|
||||
struct_exprt arg_i_struct({}, structured_type);
|
||||
std::list<exprt> field_exprs;
|
||||
for(const auto & comp : structured_type.components())
|
||||
{
|
||||
|
|
|
@ -98,7 +98,7 @@ symbol_exprt get_or_create_string_literal_symbol(
|
|||
// the literal with @clsid = String
|
||||
struct_tag_typet jlo_symbol("java::java.lang.Object");
|
||||
const auto &jlo_struct = to_struct_type(ns.follow(jlo_symbol));
|
||||
struct_exprt jlo_init(jlo_symbol);
|
||||
struct_exprt jlo_init({}, jlo_symbol);
|
||||
const auto &jls_struct = to_struct_type(ns.follow(string_type));
|
||||
java_root_class_init(jlo_init, jlo_struct, "java::java.lang.String");
|
||||
|
||||
|
@ -109,7 +109,7 @@ symbol_exprt get_or_create_string_literal_symbol(
|
|||
const array_exprt data =
|
||||
utf16_to_array(utf8_to_utf16_native_endian(id2string(value)));
|
||||
|
||||
struct_exprt literal_init(new_symbol.type);
|
||||
struct_exprt literal_init({}, new_symbol.type);
|
||||
literal_init.operands().resize(jls_struct.components().size());
|
||||
const std::size_t jlo_nb = jls_struct.component_number("@java.lang.Object");
|
||||
literal_init.operands()[jlo_nb] = jlo_init;
|
||||
|
@ -183,8 +183,7 @@ symbol_exprt get_or_create_string_literal_symbol(
|
|||
// Case where something defined java.lang.String, so it has
|
||||
// a proper base class (always java.lang.Object in practical
|
||||
// JDKs seen so far)
|
||||
struct_exprt literal_init(new_symbol.type);
|
||||
literal_init.move_to_operands(jlo_init);
|
||||
struct_exprt literal_init({std::move(jlo_init)}, new_symbol.type);
|
||||
for(const auto &comp : jls_struct.components())
|
||||
{
|
||||
if(comp.get_name()=="@java.lang.Object")
|
||||
|
|
|
@ -37,10 +37,7 @@ struct_exprt make_string_argument(std::string name)
|
|||
|
||||
const symbol_exprt length(name + "_length", length_type());
|
||||
const symbol_exprt content(name + "_content", pointer_type(java_char_type()));
|
||||
struct_exprt expr(type);
|
||||
expr.operands().push_back(length);
|
||||
expr.operands().push_back(content);
|
||||
return expr;
|
||||
return struct_exprt({length, content}, type);
|
||||
}
|
||||
|
||||
SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]")
|
||||
|
|
|
@ -39,9 +39,7 @@ SCENARIO("string_identifiers_resolution_from_equations",
|
|||
struct_typet struct_type;
|
||||
struct_type.components().emplace_back("str1", string_typet());
|
||||
struct_type.components().emplace_back("str2", string_typet());
|
||||
struct_exprt struct_expr(struct_type);
|
||||
struct_expr.operands().push_back(a);
|
||||
struct_expr.operands().push_back(f);
|
||||
struct_exprt struct_expr({a, f}, struct_type);
|
||||
symbol_exprt symbol_struct("sym_struct", struct_type);
|
||||
|
||||
std::vector<equal_exprt> equations;
|
||||
|
|
|
@ -81,7 +81,7 @@ void cpp_typecheckt::do_virtual_table(const symbolt &symbol)
|
|||
// do the values
|
||||
const struct_typet &vt_type=to_struct_type(vt_symb_type.type);
|
||||
|
||||
struct_exprt values(struct_tag_typet(vt_symb_type.name));
|
||||
struct_exprt values({}, struct_tag_typet(vt_symb_type.name));
|
||||
|
||||
for(const auto &compo : vt_type.components())
|
||||
{
|
||||
|
|
|
@ -1253,7 +1253,7 @@ void dump_ct::cleanup_expr(exprt &expr)
|
|||
{
|
||||
if(u_type_f.get_component(u.get_component_name()).get_is_padding())
|
||||
// we just use an empty struct to fake an empty union
|
||||
expr=struct_exprt(struct_typet());
|
||||
expr = struct_exprt({}, struct_typet());
|
||||
}
|
||||
// add a typecast for NULL
|
||||
else if(u.op().id()==ID_constant &&
|
||||
|
|
|
@ -465,7 +465,7 @@ exprt interpretert::get_value(
|
|||
const typet real_type=ns.follow(type);
|
||||
if(real_type.id()==ID_struct)
|
||||
{
|
||||
struct_exprt result(real_type);
|
||||
struct_exprt result({}, real_type);
|
||||
const struct_typet &struct_type=to_struct_type(real_type);
|
||||
const struct_typet::componentst &components=struct_type.components();
|
||||
|
||||
|
@ -532,7 +532,7 @@ exprt interpretert::get_value(
|
|||
|
||||
if(real_type.id()==ID_struct)
|
||||
{
|
||||
struct_exprt result(real_type);
|
||||
struct_exprt result({}, real_type);
|
||||
const struct_typet &struct_type=to_struct_type(real_type);
|
||||
const struct_typet::componentst &components=struct_type.components();
|
||||
|
||||
|
|
|
@ -136,19 +136,18 @@ static void remove_complex(exprt &expr)
|
|||
PRECONDITION(expr.operands().size() == 2);
|
||||
// do component-wise:
|
||||
// x+y -> complex(x.r+y.r,x.i+y.i)
|
||||
struct_exprt struct_expr(expr.type());
|
||||
struct_expr.operands().resize(2);
|
||||
|
||||
struct_expr.op0()=
|
||||
binary_exprt(complex_member(expr.op0(), ID_real), expr.id(),
|
||||
complex_member(expr.op1(), ID_real));
|
||||
|
||||
struct_expr.op0().add_source_location()=expr.source_location();
|
||||
|
||||
struct_expr.op1()=
|
||||
binary_exprt(complex_member(expr.op0(), ID_imag), expr.id(),
|
||||
complex_member(expr.op1(), ID_imag));
|
||||
struct_exprt struct_expr(
|
||||
{binary_exprt(
|
||||
complex_member(expr.op0(), ID_real),
|
||||
expr.id(),
|
||||
complex_member(expr.op1(), ID_real)),
|
||||
binary_exprt(
|
||||
complex_member(expr.op0(), ID_imag),
|
||||
expr.id(),
|
||||
complex_member(expr.op1(), ID_imag))},
|
||||
expr.type());
|
||||
|
||||
struct_expr.op0().add_source_location() = expr.source_location();
|
||||
struct_expr.op1().add_source_location()=expr.source_location();
|
||||
|
||||
expr=struct_expr;
|
||||
|
@ -158,18 +157,14 @@ static void remove_complex(exprt &expr)
|
|||
auto const &unary_minus_expr = to_unary_minus_expr(expr);
|
||||
// do component-wise:
|
||||
// -x -> complex(-x.r,-x.i)
|
||||
struct_exprt struct_expr(unary_minus_expr.type());
|
||||
struct_expr.operands().resize(2);
|
||||
|
||||
struct_expr.op0() =
|
||||
unary_minus_exprt(complex_member(unary_minus_expr.op(), ID_real));
|
||||
struct_exprt struct_expr(
|
||||
{unary_minus_exprt(complex_member(unary_minus_expr.op(), ID_real)),
|
||||
unary_minus_exprt(complex_member(unary_minus_expr.op(), ID_imag))},
|
||||
unary_minus_expr.type());
|
||||
|
||||
struct_expr.op0().add_source_location() =
|
||||
unary_minus_expr.source_location();
|
||||
|
||||
struct_expr.op1() =
|
||||
unary_minus_exprt(complex_member(unary_minus_expr.op(), ID_imag));
|
||||
|
||||
struct_expr.op1().add_source_location() =
|
||||
unary_minus_expr.source_location();
|
||||
|
||||
|
@ -178,9 +173,9 @@ static void remove_complex(exprt &expr)
|
|||
else if(expr.id()==ID_complex)
|
||||
{
|
||||
auto const &complex_expr = to_complex_expr(expr);
|
||||
auto struct_expr = struct_exprt(complex_expr.type());
|
||||
auto struct_expr = struct_exprt(
|
||||
{complex_expr.real(), complex_expr.imag()}, complex_expr.type());
|
||||
struct_expr.add_source_location() = complex_expr.source_location();
|
||||
struct_expr.copy_to_operands(complex_expr.real(), complex_expr.imag());
|
||||
expr.swap(struct_expr);
|
||||
}
|
||||
else if(expr.id()==ID_typecast)
|
||||
|
@ -192,18 +187,15 @@ static void remove_complex(exprt &expr)
|
|||
{
|
||||
// complex to complex -- do typecast per component
|
||||
|
||||
struct_exprt struct_expr(typecast_expr.type());
|
||||
struct_expr.operands().resize(2);
|
||||
|
||||
struct_expr.op0() =
|
||||
typecast_exprt(complex_member(typecast_expr.op(), ID_real), subtype);
|
||||
struct_exprt struct_expr(
|
||||
{typecast_exprt(complex_member(typecast_expr.op(), ID_real), subtype),
|
||||
typecast_exprt(
|
||||
complex_member(typecast_expr.op(), ID_imag), subtype)},
|
||||
typecast_expr.type());
|
||||
|
||||
struct_expr.op0().add_source_location() =
|
||||
typecast_expr.source_location();
|
||||
|
||||
struct_expr.op1() =
|
||||
typecast_exprt(complex_member(typecast_expr.op(), ID_imag), subtype);
|
||||
|
||||
struct_expr.op1().add_source_location() =
|
||||
typecast_expr.source_location();
|
||||
|
||||
|
@ -212,11 +204,10 @@ static void remove_complex(exprt &expr)
|
|||
else
|
||||
{
|
||||
// non-complex to complex
|
||||
struct_exprt struct_expr(typecast_expr.type());
|
||||
struct_expr.operands().resize(2);
|
||||
|
||||
struct_expr.op0() = typecast_exprt(typecast_expr.op(), subtype);
|
||||
struct_expr.op1()=from_integer(0, subtype);
|
||||
struct_exprt struct_expr(
|
||||
{typecast_exprt(typecast_expr.op(), subtype),
|
||||
from_integer(0, subtype)},
|
||||
typecast_expr.type());
|
||||
struct_expr.add_source_location() = typecast_expr.source_location();
|
||||
|
||||
expr=struct_expr;
|
||||
|
|
|
@ -429,12 +429,13 @@ symbol_exprt string_abstractiont::add_dummy_symbol_and_value(
|
|||
if(source_type.id()==ID_array && is_char_type(source_type.subtype()) &&
|
||||
type_eq(type, string_struct, ns))
|
||||
{
|
||||
new_symbol.value=struct_exprt(string_struct);
|
||||
new_symbol.value.operands().resize(3);
|
||||
new_symbol.value.op0()=build_unknown(whatt::IS_ZERO, false);
|
||||
new_symbol.value.op1()=build_unknown(whatt::LENGTH, false);
|
||||
new_symbol.value.op2()=to_array_type(source_type).size().id()==ID_infinity?
|
||||
build_unknown(whatt::SIZE, false):to_array_type(source_type).size();
|
||||
new_symbol.value = struct_exprt(
|
||||
{build_unknown(whatt::IS_ZERO, false),
|
||||
build_unknown(whatt::LENGTH, false),
|
||||
to_array_type(source_type).size().id() == ID_infinity
|
||||
? build_unknown(whatt::SIZE, false)
|
||||
: to_array_type(source_type).size()},
|
||||
string_struct);
|
||||
make_type(new_symbol.value.op2(), build_type(whatt::SIZE));
|
||||
}
|
||||
else
|
||||
|
@ -1032,12 +1033,11 @@ bool string_abstractiont::build_symbol_constant(
|
|||
new_symbol.is_file_local=false;
|
||||
|
||||
{
|
||||
struct_exprt value(string_struct);
|
||||
value.operands().resize(3);
|
||||
|
||||
value.op0()=true_exprt();
|
||||
value.op1()=from_integer(zero_length, build_type(whatt::LENGTH));
|
||||
value.op2()=from_integer(buf_size, build_type(whatt::SIZE));
|
||||
struct_exprt value(
|
||||
{true_exprt(),
|
||||
from_integer(zero_length, build_type(whatt::LENGTH)),
|
||||
from_integer(buf_size, build_type(whatt::SIZE))},
|
||||
string_struct);
|
||||
|
||||
// initialization
|
||||
goto_programt::targett assignment1=initialization.add_instruction();
|
||||
|
|
|
@ -152,9 +152,7 @@ exprt boolbvt::bv_get_rec(
|
|||
}
|
||||
}
|
||||
|
||||
struct_exprt dest(type);
|
||||
dest.operands().swap(op);
|
||||
return std::move(dest);
|
||||
return struct_exprt(std::move(op), type);
|
||||
}
|
||||
else if(type.id()==ID_union)
|
||||
{
|
||||
|
|
|
@ -264,7 +264,7 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
|
|||
const struct_typet::componentst &components=struct_type.components();
|
||||
|
||||
bool failed=false;
|
||||
struct_exprt s(src.type());
|
||||
struct_exprt s({}, src.type());
|
||||
|
||||
for(const auto &comp : components)
|
||||
{
|
||||
|
|
|
@ -401,10 +401,11 @@ std::pair<exprt, string_constraintst> add_axioms_for_format(
|
|||
if(fe.is_format_specifier())
|
||||
{
|
||||
const format_specifiert &fs=fe.get_format_specifier();
|
||||
struct_exprt arg;
|
||||
if(fs.conversion!=format_specifiert::PERCENT_SIGN &&
|
||||
fs.conversion!=format_specifiert::LINE_SEPARATOR)
|
||||
{
|
||||
exprt arg;
|
||||
|
||||
if(fs.index==-1)
|
||||
{
|
||||
INVARIANT(
|
||||
|
@ -421,11 +422,19 @@ std::pair<exprt, string_constraintst> add_axioms_for_format(
|
|||
// first argument `args[0]` corresponds to index 1
|
||||
arg=to_struct_expr(args[fs.index-1]);
|
||||
}
|
||||
|
||||
auto result = add_axioms_for_format_specifier(
|
||||
fresh_symbol,
|
||||
fs,
|
||||
to_struct_expr(arg),
|
||||
index_type,
|
||||
char_type,
|
||||
array_pool,
|
||||
message,
|
||||
ns);
|
||||
merge(constraints, std::move(result.second));
|
||||
intermediary_strings.push_back(result.first);
|
||||
}
|
||||
auto result = add_axioms_for_format_specifier(
|
||||
fresh_symbol, fs, arg, index_type, char_type, array_pool, message, ns);
|
||||
merge(constraints, std::move(result.second));
|
||||
intermediary_strings.push_back(result.first);
|
||||
}
|
||||
else
|
||||
{
|
||||
|
|
|
@ -393,9 +393,7 @@ exprt smt2_convt::parse_struct(
|
|||
const struct_typet::componentst &components =
|
||||
type.components();
|
||||
|
||||
struct_exprt result(type);
|
||||
|
||||
result.operands().resize(components.size(), nil_exprt());
|
||||
struct_exprt result(exprt::operandst(components.size(), nil_exprt()), type);
|
||||
|
||||
if(components.empty())
|
||||
return std::move(result);
|
||||
|
|
|
@ -188,7 +188,7 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
|
|||
const struct_typet::componentst &components=
|
||||
to_struct_type(type).components();
|
||||
|
||||
struct_exprt value(type);
|
||||
struct_exprt value({}, type);
|
||||
|
||||
value.operands().reserve(components.size());
|
||||
|
||||
|
|
|
@ -1492,7 +1492,7 @@ exprt simplify_exprt::bits2expr(
|
|||
const struct_typet::componentst &components=
|
||||
struct_type.components();
|
||||
|
||||
struct_exprt result(type);
|
||||
struct_exprt result({}, type);
|
||||
result.reserve_operands(components.size());
|
||||
|
||||
mp_integer m_offset_bits=0;
|
||||
|
|
|
@ -1959,6 +1959,11 @@ public:
|
|||
{
|
||||
}
|
||||
|
||||
struct_exprt(operandst &&_operands, const typet &_type)
|
||||
: multi_ary_exprt(ID_struct, std::move(_operands), _type)
|
||||
{
|
||||
}
|
||||
|
||||
exprt &component(const irep_idt &name, const namespacet &ns);
|
||||
const exprt &component(const irep_idt &name, const namespacet &ns) const;
|
||||
};
|
||||
|
|
|
@ -123,9 +123,8 @@ public:
|
|||
const exprt &_length,
|
||||
const exprt &_content,
|
||||
const typet &type)
|
||||
: struct_exprt(type)
|
||||
: struct_exprt({_length, _content}, type)
|
||||
{
|
||||
add_to_operands(_length, _content);
|
||||
}
|
||||
|
||||
refined_string_exprt(const exprt &_length, const exprt &_content)
|
||||
|
|
|
@ -211,11 +211,10 @@ SCENARIO(
|
|||
|
||||
WHEN("We query what '{ .x = &a2, .y = &a3 }.x' points to")
|
||||
{
|
||||
struct_exprt struct_constant(struct_tag_typet(A_symbol.name));
|
||||
struct_constant.copy_to_operands(
|
||||
address_of_exprt(a2_symbol.symbol_expr()));
|
||||
struct_constant.copy_to_operands(
|
||||
address_of_exprt(a3_symbol.symbol_expr()));
|
||||
struct_exprt struct_constant(
|
||||
{address_of_exprt(a2_symbol.symbol_expr()),
|
||||
address_of_exprt(a3_symbol.symbol_expr())},
|
||||
struct_tag_typet(A_symbol.name));
|
||||
|
||||
member_exprt member_of_constant(struct_constant, A_x);
|
||||
|
||||
|
|
Loading…
Reference in New Issue