Skip to content

Commit 4269207

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 1ba3a16 commit 4269207

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
@@ -1558,14 +1558,14 @@ code_blockt java_string_library_preprocesst::make_object_get_class_code(
15581558
loc);
15591559

15601560
// > class1 = Class.forName(string1)
1561+
java_method_typet fun_type(
1562+
{java_method_typet::parametert(string_ptr_type)}, class_type);
15611563
code_function_callt fun_call(
15621564
class1,
15631565
symbol_exprt(
1564-
"java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;"),
1566+
"java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;",
1567+
std::move(fun_type)),
15651568
{string1});
1566-
const java_method_typet fun_type(
1567-
{java_method_typet::parametert(string_ptr_type)}, class_type);
1568-
fun_call.function().type()=fun_type;
15691569
code.add(fun_call, loc);
15701570

15711571
// > 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
@@ -68,19 +68,19 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]")
6868

6969
// fun1 is s3 = s1.concat(s2)
7070
const function_application_exprt fun1(
71-
symbol_exprt(ID_cprover_string_concat_func),
71+
symbol_exprt(ID_cprover_string_concat_func, typet()),
7272
{string3.op0(), string3.op1(), string1, string2},
7373
fun_type);
7474

7575
// fun2 is s5 = s3.concat(s4)
7676
const function_application_exprt fun2(
77-
symbol_exprt(ID_cprover_string_concat_func),
77+
symbol_exprt(ID_cprover_string_concat_func, typet()),
7878
{string5.op0(), string5.op1(), string3, string4},
7979
fun_type);
8080

8181
// fun3 is s6 = s5.concat(s2)
8282
const function_application_exprt fun3(
83-
symbol_exprt(ID_cprover_string_concat_func),
83+
symbol_exprt(ID_cprover_string_concat_func, typet()),
8484
{string6.op0(), string6.op1(), string5, string2},
8585
fun_type);
8686

‎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
@@ -1451,13 +1451,11 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
14511451
throw 0;
14521452
}
14531453

1454-
symbol_exprt result;
1455-
result.add_source_location()=source_location;
1456-
result.set_identifier(identifier);
14571454
code_typet t(
14581455
{code_typet::parametert(ptr_arg.type())}, ptr_arg.type().subtype());
14591456
t.make_ellipsis();
1460-
result.type()=t;
1457+
symbol_exprt result(identifier, t);
1458+
result.add_source_location() = source_location;
14611459
expr.swap(result);
14621460
return;
14631461
}
@@ -1484,14 +1482,12 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
14841482
throw 0;
14851483
}
14861484

1487-
symbol_exprt result;
1488-
result.add_source_location()=source_location;
1489-
result.set_identifier(identifier);
14901485
const code_typet t(
14911486
{code_typet::parametert(ptr_arg.type()),
14921487
code_typet::parametert(signed_int_type())},
14931488
ptr_arg.type().subtype());
1494-
result.type()=t;
1489+
symbol_exprt result(identifier, t);
1490+
result.add_source_location() = source_location;
14951491
expr.swap(result);
14961492
return;
14971493
}
@@ -1518,15 +1514,13 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
15181514
throw 0;
15191515
}
15201516

1521-
symbol_exprt result;
1522-
result.add_source_location()=source_location;
1523-
result.set_identifier(identifier);
15241517
const code_typet t(
15251518
{code_typet::parametert(ptr_arg.type()),
15261519
code_typet::parametert(ptr_arg.type().subtype()),
15271520
code_typet::parametert(signed_int_type())},
15281521
empty_typet());
1529-
result.type()=t;
1522+
symbol_exprt result(identifier, t);
1523+
result.add_source_location() = source_location;
15301524
expr.swap(result);
15311525
return;
15321526
}
@@ -1553,15 +1547,13 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
15531547
throw 0;
15541548
}
15551549

1556-
symbol_exprt result;
1557-
result.add_source_location()=source_location;
1558-
result.set_identifier(identifier);
15591550
const code_typet t(
15601551
{code_typet::parametert(ptr_arg.type()),
15611552
code_typet::parametert(ptr_arg.type().subtype()),
15621553
code_typet::parametert(signed_int_type())},
15631554
ptr_arg.type().subtype());
1564-
result.type()=t;
1555+
symbol_exprt result(identifier, t);
1556+
result.add_source_location() = source_location;
15651557
expr.swap(result);
15661558
return;
15671559
}
@@ -1596,15 +1588,13 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
15961588

15971589
const exprt &ptr_arg=fargs.operands.front();
15981590

1599-
symbol_exprt result;
1600-
result.add_source_location()=source_location;
1601-
result.set_identifier(identifier);
16021591
const code_typet t(
16031592
{code_typet::parametert(ptr_arg.type()),
16041593
code_typet::parametert(ptr_arg.type()),
16051594
code_typet::parametert(signed_int_type())},
16061595
empty_typet());
1607-
result.type()=t;
1596+
symbol_exprt result(identifier, t);
1597+
result.add_source_location() = source_location;
16081598
expr.swap(result);
16091599
return;
16101600
}
@@ -1645,16 +1635,14 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
16451635

16461636
const exprt &ptr_arg=fargs.operands.front();
16471637

1648-
symbol_exprt result;
1649-
result.add_source_location()=source_location;
1650-
result.set_identifier(identifier);
16511638
const code_typet t(
16521639
{code_typet::parametert(ptr_arg.type()),
16531640
code_typet::parametert(ptr_arg.type()),
16541641
code_typet::parametert(ptr_arg.type()),
16551642
code_typet::parametert(signed_int_type())},
16561643
empty_typet());
1657-
result.type()=t;
1644+
symbol_exprt result(identifier, t);
1645+
result.add_source_location() = source_location;
16581646
expr.swap(result);
16591647
return;
16601648
}
@@ -1700,9 +1688,6 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
17001688

17011689
const exprt &ptr_arg=fargs.operands.front();
17021690

1703-
symbol_exprt result;
1704-
result.add_source_location()=source_location;
1705-
result.set_identifier(identifier);
17061691
code_typet::parameterst parameters;
17071692
parameters.push_back(code_typet::parametert(ptr_arg.type()));
17081693
parameters.push_back(code_typet::parametert(ptr_arg.type()));
@@ -1716,7 +1701,8 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
17161701
parameters.push_back(code_typet::parametert(signed_int_type()));
17171702
parameters.push_back(code_typet::parametert(signed_int_type()));
17181703
code_typet t(std::move(parameters), c_bool_type());
1719-
result.type()=t;
1704+
symbol_exprt result(identifier, t);
1705+
result.add_source_location() = source_location;
17201706
expr.swap(result);
17211707
return;
17221708
}
@@ -1745,13 +1731,11 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
17451731
throw 0;
17461732
}
17471733

1748-
symbol_exprt result;
1749-
result.add_source_location()=source_location;
1750-
result.set_identifier(identifier);
17511734
code_typet t(
17521735
{code_typet::parametert(ptr_arg.type())}, ptr_arg.type().subtype());
17531736
t.make_ellipsis();
1754-
result.type()=t;
1737+
symbol_exprt result(identifier, t);
1738+
result.add_source_location() = source_location;
17551739
expr.swap(result);
17561740
return;
17571741
}
@@ -1780,13 +1764,11 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
17801764
throw 0;
17811765
}
17821766

1783-
symbol_exprt result;
1784-
result.add_source_location()=source_location;
1785-
result.set_identifier(identifier);
17861767
code_typet t(
17871768
{code_typet::parametert(ptr_arg.type())}, ptr_arg.type().subtype());
17881769
t.make_ellipsis();
1789-
result.type()=t;
1770+
symbol_exprt result(identifier, t);
1771+
result.add_source_location() = source_location;
17901772
expr.swap(result);
17911773
return;
17921774
}

0 commit comments

Comments
 (0)