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

Construct struct_exprt in a non-deprecated way 

The existing struct_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 17:52:13 +00:00
parent 80cb920a68
commit 3e82e5b0cf
17 changed files with 65 additions and 84 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
jbmc/src/java_bytecode/java_string_library_preprocess.cpp
View File

@ -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())
{

7
jbmc/src/java_bytecode/java_string_literals.cpp
View File

@ -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")

5
jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp
View File

@ -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]")

4
jbmc/unit/solvers/refinement/string_refinement/string_symbol_resolution.cpp
View File

@ -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;

2
src/cpp/cpp_typecheck_virtual_table.cpp
View File

@ -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())
{

2
src/goto-instrument/dump_c.cpp
View File

@ -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 &&

4
src/goto-programs/interpreter.cpp
View File

@ -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();

61
src/goto-programs/remove_complex.cpp
View File

@ -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;

24
src/goto-programs/string_abstraction.cpp
View File

@ -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();

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

@ -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)
{

2
src/solvers/lowering/byte_operators.cpp
View File

@ -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)
{

4
src/solvers/smt2/smt2_conv.cpp
View File

@ -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);

2
src/util/expr_initializer.cpp
View File

@ -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());

2
src/util/simplify_expr.cpp
View File

@ -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;

5
src/util/std_expr.h
View File

@ -1944,6 +1944,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;
};

3
src/util/string_expr.h
View File

@ -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)

9
unit/pointer-analysis/value_set.cpp
View File

@ -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);