Skip to content

Commit 786fde7

Browse files
tautschnigtautschnig
committed
Replace all uses of deprecated symbol_exprt constructors
This helps type safety has it avoids constructing symbol_exprts that never get a proper type (or identifier).
1 parent 73ebbb4 commit 786fde7

39 files changed

+138
-152
lines changed

‎jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1536,13 +1536,12 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
15361536
else if(statement=="getstatic")
15371537
{
15381538
PRECONDITION(op.empty() && results.size() == 1);
1539-
symbol_exprt symbol_expr(arg0.type());
15401539
const auto &field_name=arg0.get_string(ID_component_name);
15411540
const bool is_assertions_disabled_field=
15421541
field_name.find("$assertionsDisabled")!=std::string::npos;
15431542

1544-
symbol_expr.set_identifier(
1545-
get_static_field(arg0.get_string(ID_class), field_name));
1543+
const symbol_exprt symbol_expr(
1544+
get_static_field(arg0.get_string(ID_class), field_name), arg0.type());
15461545

15471546
INVARIANT(
15481547
symbol_table.has_symbol(symbol_expr.get_identifier()),
@@ -1559,10 +1558,10 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
15591558
else if(statement=="putstatic")
15601559
{
15611560
PRECONDITION(op.size() == 1 && results.empty());
1562-
symbol_exprt symbol_expr(arg0.type());
15631561
const auto &field_name=arg0.get_string(ID_component_name);
1564-
symbol_expr.set_identifier(
1565-
get_static_field(arg0.get_string(ID_class), field_name));
1562+
1563+
const symbol_exprt symbol_expr(
1564+
get_static_field(arg0.get_string(ID_class), field_name), arg0.type());
15661565

15671566
INVARIANT(
15681567
symbol_table.has_symbol(symbol_expr.get_identifier()),

‎jbmc/src/java_bytecode/java_bytecode_convert_method_class.h

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -119,7 +119,11 @@ class java_bytecode_convert_methodt:public messaget
119119
bool is_parameter;
120120
std::vector<holet> holes;
121121

122-
variablet() : symbol_expr(), start_pc(0), length(0), is_parameter(false)
122+
variablet()
123+
: symbol_expr("", typet()),
124+
start_pc(0),
125+
length(0),
126+
is_parameter(false)
123127
{
124128
}
125129
};

‎jbmc/src/java_bytecode/java_bytecode_parser.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1600,7 +1600,7 @@ exprt java_bytecode_parsert::get_relement_value()
16001600
case 'c':
16011601
{
16021602
u2 class_info_index = read_u2();
1603-
return symbol_exprt(pool_entry(class_info_index).s);
1603+
return symbol_exprt(pool_entry(class_info_index).s, typet());
16041604
}
16051605

16061606
case '@':

‎jbmc/src/java_bytecode/java_string_library_preprocess.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1555,14 +1555,14 @@ code_blockt java_string_library_preprocesst::make_object_get_class_code(
15551555
loc);
15561556

15571557
// > class1 = Class.forName(string1)
1558+
java_method_typet fun_type(
1559+
{java_method_typet::parametert(string_ptr_type)}, class_type);
15581560
code_function_callt fun_call(
15591561
class1,
15601562
symbol_exprt(
1561-
"java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;"),
1563+
"java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;",
1564+
std::move(fun_type)),
15621565
{string1});
1563-
const java_method_typet fun_type(
1564-
{java_method_typet::parametert(string_ptr_type)}, class_type);
1565-
fun_call.function().type()=fun_type;
15661566
code.add(fun_call, loc);
15671567

15681568
// > return class1;

‎jbmc/src/java_bytecode/java_utils.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -285,7 +285,8 @@ exprt make_function_application(
285285
declare_function(fun_name, type, symbol_table);
286286

287287
// Function application
288-
return function_application_exprt(symbol_exprt(fun_name), arguments, type);
288+
return function_application_exprt(
289+
symbol_exprt(fun_name, typet()), arguments, type);
289290
}
290291

291292
/// Strip java:: prefix from given identifier

‎jbmc/src/java_bytecode/simple_method_stubbing.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -170,7 +170,8 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol)
170170
symbol_table);
171171
const symbol_exprt &init_symbol_expression = init_symbol.symbol_expr();
172172
code_assignt get_argument(
173-
init_symbol_expression, symbol_exprt(this_argument.get_identifier()));
173+
init_symbol_expression,
174+
symbol_exprt(this_argument.get_identifier(), this_argument.type()));
174175
get_argument.add_source_location() = synthesized_source_location;
175176
new_instructions.add(get_argument);
176177
create_method_stub_at(

‎jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -185,7 +185,7 @@ SCENARIO("instantiate_not_contains",
185185
{
186186
// Creating "ab".lastIndexOf("b", 0)
187187
const function_application_exprt func(
188-
symbol_exprt(ID_cprover_string_last_index_of_func),
188+
symbol_exprt(ID_cprover_string_last_index_of_func, typet()),
189189
{ab, b, from_integer(2)},
190190
t.length_type());
191191

@@ -215,7 +215,7 @@ SCENARIO("instantiate_not_contains",
215215
simplify(sc.premise, empty_ns);
216216
simplify(sc.s0, empty_ns);
217217
simplify(sc.s1, empty_ns);
218-
witnesses[sc] = generator.fresh_symbol("w", t.witness_type());
218+
witnesses.emplace(sc, generator.fresh_symbol("w", t.witness_type()));
219219
nc_axioms.push_back(sc);
220220
return accu + to_string(sc) + "\n\n";
221221
});
@@ -287,7 +287,7 @@ SCENARIO("instantiate_not_contains",
287287
// Create witness for axiom
288288
string_constraint_generatort generator(empty_ns);
289289
std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
290-
witnesses[vacuous] = generator.fresh_symbol("w", t.witness_type());
290+
witnesses.emplace(vacuous, generator.fresh_symbol("w", t.witness_type()));
291291

292292
INFO("Original axiom:\n");
293293
INFO(to_string(vacuous) + "\n\n");
@@ -337,7 +337,7 @@ SCENARIO("instantiate_not_contains",
337337
// Create witness for axiom
338338
string_constraint_generatort generator(empty_ns);
339339
std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
340-
witnesses[trivial] = generator.fresh_symbol("w", t.witness_type());
340+
witnesses.emplace(trivial, generator.fresh_symbol("w", t.witness_type()));
341341

342342
INFO("Original axiom:\n");
343343
INFO(to_string(trivial) + "\n\n");
@@ -388,7 +388,7 @@ SCENARIO("instantiate_not_contains",
388388
// Create witness for axiom
389389
string_constraint_generatort generator(empty_ns);
390390
std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
391-
witnesses[trivial] = generator.fresh_symbol("w", t.witness_type());
391+
witnesses.emplace(trivial, generator.fresh_symbol("w", t.witness_type()));
392392

393393
INFO("Original axiom:\n");
394394
INFO(to_string(trivial) + "\n\n");
@@ -441,7 +441,7 @@ SCENARIO("instantiate_not_contains",
441441
// Create witness for axiom
442442
string_constraint_generatort generator(empty_ns);
443443
std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
444-
witnesses[trivial] = generator.fresh_symbol("w", t.witness_type());
444+
witnesses.emplace(trivial, generator.fresh_symbol("w", t.witness_type()));
445445

446446
INFO("Original axiom:\n");
447447
INFO(to_string(trivial) + "\n\n");
@@ -492,7 +492,7 @@ SCENARIO("instantiate_not_contains",
492492
// Create witness for axiom
493493
string_constraint_generatort generator(empty_ns);
494494
std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
495-
witnesses[trivial] = generator.fresh_symbol("w", t.witness_type());
495+
witnesses.emplace(trivial, generator.fresh_symbol("w", t.witness_type()));
496496

497497
INFO("Original axiom:\n");
498498
INFO(to_string(trivial) + "\n\n");

‎jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -65,19 +65,19 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]")
6565

6666
// fun1 is s3 = s1.concat(s2)
6767
const function_application_exprt fun1(
68-
symbol_exprt(ID_cprover_string_concat_func),
68+
symbol_exprt(ID_cprover_string_concat_func, typet()),
6969
{string3.op0(), string3.op1(), string1, string2},
7070
fun_type);
7171

7272
// fun2 is s5 = s3.concat(s4)
7373
const function_application_exprt fun2(
74-
symbol_exprt(ID_cprover_string_concat_func),
74+
symbol_exprt(ID_cprover_string_concat_func, typet()),
7575
{string5.op0(), string5.op1(), string3, string4},
7676
fun_type);
7777

7878
// fun3 is s6 = s5.concat(s2)
7979
const function_application_exprt fun3(
80-
symbol_exprt(ID_cprover_string_concat_func),
80+
symbol_exprt(ID_cprover_string_concat_func, typet()),
8181
{string6.op0(), string6.op1(), string5, string2},
8282
fun_type);
8383

‎src/analyses/constant_propagator.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -649,7 +649,8 @@ bool constant_propagator_domaint::partial_evaluate(
649649
// if the current rounding mode is top we can
650650
// still get a non-top result by trying all rounding
651651
// modes and checking if the results are all the same
652-
if(!known_values.is_constant(symbol_exprt(ID_cprover_rounding_mode_str)))
652+
if(!known_values.is_constant(
653+
symbol_exprt(ID_cprover_rounding_mode_str, typet())))
653654
{
654655
return partial_evaluate_with_all_rounding_modes(known_values, expr, ns);
655656
}

‎src/analyses/locals.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -21,12 +21,13 @@ void localst::build(const goto_functiont &goto_function)
2121
if(it->is_decl())
2222
{
2323
const code_declt &code_decl=to_code_decl(it->code);
24-
locals_map[code_decl.get_identifier()] = code_decl.symbol();
24+
locals_map.emplace(code_decl.get_identifier(), code_decl.symbol());
2525
}
2626

2727
for(const auto &param : goto_function.type.parameters())
28-
locals_map[param.get_identifier()]=
29-
symbol_exprt(param.get_identifier(), param.type());
28+
locals_map.emplace(
29+
param.get_identifier(),
30+
symbol_exprt(param.get_identifier(), param.type()));
3031
}
3132

3233
void localst::output(std::ostream &out) const

‎src/ansi-c/c_typecheck_base.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -697,9 +697,9 @@ void c_typecheck_baset::typecheck_declaration(
697697
// also cater for renaming/placement in sections
698698
const auto &renaming_entry = asm_label_map.find(full_spec.alias);
699699
if(renaming_entry == asm_label_map.end())
700-
symbol.value = symbol_exprt(full_spec.alias);
700+
symbol.value = symbol_exprt(full_spec.alias, typet());
701701
else
702-
symbol.value = symbol_exprt(renaming_entry->second);
702+
symbol.value = symbol_exprt(renaming_entry->second, typet());
703703
symbol.is_macro=true;
704704
}
705705

‎src/ansi-c/c_typecheck_type.cpp

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -635,9 +635,7 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type)
635635
symbol_table.add(new_symbol);
636636

637637
// produce the code that declares and initializes the symbol
638-
symbol_exprt symbol_expr;
639-
symbol_expr.set_identifier(temp_identifier);
640-
symbol_expr.type()=new_symbol.type;
638+
symbol_exprt symbol_expr(temp_identifier, new_symbol.type);
641639

642640
code_declt declaration(symbol_expr);
643641
declaration.add_source_location() = size_source_location;

‎src/cpp/cpp_typecheck_compound_type.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -743,8 +743,7 @@ void cpp_typecheckt::typecheck_compound_declarator(
743743
}
744744
else
745745
{
746-
symbol_exprt symexpr;
747-
symexpr.set_identifier(new_symbol->name);
746+
symbol_exprt symexpr(new_symbol->name, typet());
748747

749748
exprt::operandst ops;
750749
ops.push_back(value);

‎src/cpp/cpp_typecheck_expr.cpp

Lines changed: 18 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -1445,13 +1445,11 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
14451445
throw 0;
14461446
}
14471447

1448-
symbol_exprt result;
1449-
result.add_source_location()=source_location;
1450-
result.set_identifier(identifier);
14511448
code_typet t(
14521449
{code_typet::parametert(ptr_arg.type())}, ptr_arg.type().subtype());
14531450
t.make_ellipsis();
1454-
result.type()=t;
1451+
symbol_exprt result(identifier, t);
1452+
result.add_source_location() = source_location;
14551453
expr.swap(result);
14561454
return;
14571455
}
@@ -1478,14 +1476,12 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
14781476
throw 0;
14791477
}
14801478

1481-
symbol_exprt result;
1482-
result.add_source_location()=source_location;
1483-
result.set_identifier(identifier);
14841479
const code_typet t(
14851480
{code_typet::parametert(ptr_arg.type()),
14861481
code_typet::parametert(signed_int_type())},
14871482
ptr_arg.type().subtype());
1488-
result.type()=t;
1483+
symbol_exprt result(identifier, t);
1484+
result.add_source_location() = source_location;
14891485
expr.swap(result);
14901486
return;
14911487
}
@@ -1512,15 +1508,13 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
15121508
throw 0;
15131509
}
15141510

1515-
symbol_exprt result;
1516-
result.add_source_location()=source_location;
1517-
result.set_identifier(identifier);
15181511
const code_typet t(
15191512
{code_typet::parametert(ptr_arg.type()),
15201513
code_typet::parametert(ptr_arg.type().subtype()),
15211514
code_typet::parametert(signed_int_type())},
15221515
empty_typet());
1523-
result.type()=t;
1516+
symbol_exprt result(identifier, t);
1517+
result.add_source_location() = source_location;
15241518
expr.swap(result);
15251519
return;
15261520
}
@@ -1547,15 +1541,13 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
15471541
throw 0;
15481542
}
15491543

1550-
symbol_exprt result;
1551-
result.add_source_location()=source_location;
1552-
result.set_identifier(identifier);
15531544
const code_typet t(
15541545
{code_typet::parametert(ptr_arg.type()),
15551546
code_typet::parametert(ptr_arg.type().subtype()),
15561547
code_typet::parametert(signed_int_type())},
15571548
ptr_arg.type().subtype());
1558-
result.type()=t;
1549+
symbol_exprt result(identifier, t);
1550+
result.add_source_location() = source_location;
15591551
expr.swap(result);
15601552
return;
15611553
}
@@ -1590,15 +1582,13 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
15901582

15911583
const exprt &ptr_arg=fargs.operands.front();
15921584

1593-
symbol_exprt result;
1594-
result.add_source_location()=source_location;
1595-
result.set_identifier(identifier);
15961585
const code_typet t(
15971586
{code_typet::parametert(ptr_arg.type()),
15981587
code_typet::parametert(ptr_arg.type()),
15991588
code_typet::parametert(signed_int_type())},
16001589
empty_typet());
1601-
result.type()=t;
1590+
symbol_exprt result(identifier, t);
1591+
result.add_source_location() = source_location;
16021592
expr.swap(result);
16031593
return;
16041594
}
@@ -1639,16 +1629,14 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
16391629

16401630
const exprt &ptr_arg=fargs.operands.front();
16411631

1642-
symbol_exprt result;
1643-
result.add_source_location()=source_location;
1644-
result.set_identifier(identifier);
16451632
const code_typet t(
16461633
{code_typet::parametert(ptr_arg.type()),
16471634
code_typet::parametert(ptr_arg.type()),
16481635
code_typet::parametert(ptr_arg.type()),
16491636
code_typet::parametert(signed_int_type())},
16501637
empty_typet());
1651-
result.type()=t;
1638+
symbol_exprt result(identifier, t);
1639+
result.add_source_location() = source_location;
16521640
expr.swap(result);
16531641
return;
16541642
}
@@ -1694,9 +1682,6 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
16941682

16951683
const exprt &ptr_arg=fargs.operands.front();
16961684

1697-
symbol_exprt result;
1698-
result.add_source_location()=source_location;
1699-
result.set_identifier(identifier);
17001685
code_typet::parameterst parameters;
17011686
parameters.push_back(code_typet::parametert(ptr_arg.type()));
17021687
parameters.push_back(code_typet::parametert(ptr_arg.type()));
@@ -1710,7 +1695,8 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
17101695
parameters.push_back(code_typet::parametert(signed_int_type()));
17111696
parameters.push_back(code_typet::parametert(signed_int_type()));
17121697
code_typet t(std::move(parameters), c_bool_type());
1713-
result.type()=t;
1698+
symbol_exprt result(identifier, t);
1699+
result.add_source_location() = source_location;
17141700
expr.swap(result);
17151701
return;
17161702
}
@@ -1739,13 +1725,11 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
17391725
throw 0;
17401726
}
17411727

1742-
symbol_exprt result;
1743-
result.add_source_location()=source_location;
1744-
result.set_identifier(identifier);
17451728
code_typet t(
17461729
{code_typet::parametert(ptr_arg.type())}, ptr_arg.type().subtype());
17471730
t.make_ellipsis();
1748-
result.type()=t;
1731+
symbol_exprt result(identifier, t);
1732+
result.add_source_location() = source_location;
17491733
expr.swap(result);
17501734
return;
17511735
}
@@ -1774,13 +1758,11 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
17741758
throw 0;
17751759
}
17761760

1777-
symbol_exprt result;
1778-
result.add_source_location()=source_location;
1779-
result.set_identifier(identifier);
17801761
code_typet t(
17811762
{code_typet::parametert(ptr_arg.type())}, ptr_arg.type().subtype());
17821763
t.make_ellipsis();
1783-
result.type()=t;
1764+
symbol_exprt result(identifier, t);
1765+
result.add_source_location() = source_location;
17841766
expr.swap(result);
17851767
return;
17861768
}

0 commit comments

Comments
 (0)