Skip to content

Commit 30dafe2

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 6f06664 commit 30dafe2

38 files changed

+136
-151
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
@@ -1560,14 +1560,14 @@ code_blockt java_string_library_preprocesst::make_object_get_class_code(
15601560
loc);
15611561

15621562
// > class1 = Class.forName(string1)
1563+
java_method_typet fun_type(
1564+
{java_method_typet::parametert(string_ptr_type)}, class_type);
15631565
code_function_callt fun_call(
15641566
class1,
15651567
symbol_exprt(
1566-
"java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;"),
1568+
"java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;",
1569+
std::move(fun_type)),
15671570
{string1});
1568-
const java_method_typet fun_type(
1569-
{java_method_typet::parametert(string_ptr_type)}, class_type);
1570-
fun_call.function().type()=fun_type;
15711571
code.add(fun_call, loc);
15721572

15731573
// > 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/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

0 commit comments

Comments
 (0)