Skip to content

Commit 7f2e159

Browse files
tautschnigtautschnig
committed
Rewrite use of *_nonconst()
Construct instructions with the intended value right away rather than fixing them up afterwards.
1 parent 0015602 commit 7f2e159

File tree

6 files changed

+180
-199
lines changed

6 files changed

+180
-199
lines changed

‎src/goto-programs/builtin_functions.cpp

Lines changed: 43 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -692,11 +692,11 @@ void goto_convertt::do_function_call_symbol(
692692
}
693693

694694
// let's double-check the type of the argument
695-
goto_programt::targett t = dest.add(goto_programt::make_assumption(
695+
source_locationt annotated_location = function.source_location();
696+
annotated_location.set("user-provided", true);
697+
dest.add(goto_programt::make_assumption(
696698
typecast_exprt::conditional_cast(arguments.front(), bool_typet()),
697-
function.source_location()));
698-
699-
t->source_location_nonconst().set("user-provided", true);
699+
annotated_location));
700700

701701
if(lhs.is_not_nil())
702702
{
@@ -714,11 +714,10 @@ void goto_convertt::do_function_call_symbol(
714714
throw 0;
715715
}
716716

717-
goto_programt::targett t = dest.add(
718-
goto_programt::make_assertion(false_exprt(), function.source_location()));
719-
720-
t->source_location_nonconst().set("user-provided", true);
721-
t->source_location_nonconst().set_property_class(ID_assertion);
717+
source_locationt annotated_location = function.source_location();
718+
annotated_location.set("user-provided", true);
719+
annotated_location.set_property_class(ID_assertion);
720+
dest.add(goto_programt::make_assertion(false_exprt(), annotated_location));
722721

723722
if(lhs.is_not_nil())
724723
{
@@ -729,9 +728,9 @@ void goto_convertt::do_function_call_symbol(
729728

730729
// __VERIFIER_error has abort() semantics, even if no assertions
731730
// are being checked
732-
goto_programt::targett a = dest.add(goto_programt::make_assumption(
733-
false_exprt(), function.source_location()));
734-
a->source_location_nonconst().set("user-provided", true);
731+
annotated_location = function.source_location();
732+
annotated_location.set("user-provided", true);
733+
dest.add(goto_programt::make_assumption(false_exprt(), annotated_location));
735734
}
736735
else if(
737736
identifier == "assert" &&
@@ -745,13 +744,14 @@ void goto_convertt::do_function_call_symbol(
745744
}
746745

747746
// let's double-check the type of the argument
748-
goto_programt::targett t = dest.add(goto_programt::make_assertion(
749-
typecast_exprt::conditional_cast(arguments.front(), bool_typet()),
750-
function.source_location()));
751-
t->source_location_nonconst().set("user-provided", true);
752-
t->source_location_nonconst().set_property_class(ID_assertion);
753-
t->source_location_nonconst().set_comment(
747+
source_locationt annotated_location = function.source_location();
748+
annotated_location.set("user-provided", true);
749+
annotated_location.set_property_class(ID_assertion);
750+
annotated_location.set_comment(
754751
"assertion " + from_expr(ns, identifier, arguments.front()));
752+
dest.add(goto_programt::make_assertion(
753+
typecast_exprt::conditional_cast(arguments.front(), bool_typet()),
754+
annotated_location));
755755

756756
if(lhs.is_not_nil())
757757
{
@@ -784,26 +784,27 @@ void goto_convertt::do_function_call_symbol(
784784
get_string_constant(arguments[1]);
785785

786786
// let's double-check the type of the argument
787-
goto_programt::targett t = dest.add(goto_programt::make_assertion(
788-
typecast_exprt::conditional_cast(arguments[0], bool_typet()),
789-
function.source_location()));
790-
787+
source_locationt annotated_location = function.source_location();
791788
if(is_precondition)
792789
{
793-
t->source_location_nonconst().set_property_class(ID_precondition);
790+
annotated_location.set_property_class(ID_precondition);
794791
}
795792
else if(is_postcondition)
796793
{
797-
t->source_location_nonconst().set_property_class(ID_postcondition);
794+
annotated_location.set_property_class(ID_postcondition);
798795
}
799796
else
800797
{
801-
t->source_location_nonconst().set(
798+
annotated_location.set(
802799
"user-provided", !function.source_location().is_built_in());
803-
t->source_location_nonconst().set_property_class(ID_assertion);
800+
annotated_location.set_property_class(ID_assertion);
804801
}
805802

806-
t->source_location_nonconst().set_comment(description);
803+
annotated_location.set_comment(description);
804+
805+
dest.add(goto_programt::make_assertion(
806+
typecast_exprt::conditional_cast(arguments[0], bool_typet()),
807+
annotated_location));
807808

808809
if(lhs.is_not_nil())
809810
{
@@ -995,12 +996,11 @@ void goto_convertt::do_function_call_symbol(
995996
const irep_idt description=
996997
"assertion "+id2string(get_string_constant(arguments[0]));
997998

998-
goto_programt::targett t = dest.add(
999-
goto_programt::make_assertion(false_exprt(), function.source_location()));
1000-
1001-
t->source_location_nonconst().set("user-provided", true);
1002-
t->source_location_nonconst().set_property_class(ID_assertion);
1003-
t->source_location_nonconst().set_comment(description);
999+
source_locationt annotated_location = function.source_location();
1000+
annotated_location.set("user-provided", true);
1001+
annotated_location.set_property_class(ID_assertion);
1002+
annotated_location.set_comment(description);
1003+
dest.add(goto_programt::make_assertion(false_exprt(), annotated_location));
10041004
// we ignore any LHS
10051005
}
10061006
else if(identifier=="__assert_rtn" ||
@@ -1033,12 +1033,11 @@ void goto_convertt::do_function_call_symbol(
10331033
throw 0;
10341034
}
10351035

1036-
goto_programt::targett t = dest.add(
1037-
goto_programt::make_assertion(false_exprt(), function.source_location()));
1038-
1039-
t->source_location_nonconst().set("user-provided", true);
1040-
t->source_location_nonconst().set_property_class(ID_assertion);
1041-
t->source_location_nonconst().set_comment(description);
1036+
source_locationt annotated_location = function.source_location();
1037+
annotated_location.set("user-provided", true);
1038+
annotated_location.set_property_class(ID_assertion);
1039+
annotated_location.set_comment(description);
1040+
dest.add(goto_programt::make_assertion(false_exprt(), annotated_location));
10421041
// we ignore any LHS
10431042
}
10441043
else if(identifier=="__assert_func")
@@ -1067,12 +1066,11 @@ void goto_convertt::do_function_call_symbol(
10671066
description="assertion";
10681067
}
10691068

1070-
goto_programt::targett t = dest.add(
1071-
goto_programt::make_assertion(false_exprt(), function.source_location()));
1072-
1073-
t->source_location_nonconst().set("user-provided", true);
1074-
t->source_location_nonconst().set_property_class(ID_assertion);
1075-
t->source_location_nonconst().set_comment(description);
1069+
source_locationt annotated_location = function.source_location();
1070+
annotated_location.set("user-provided", true);
1071+
annotated_location.set_property_class(ID_assertion);
1072+
annotated_location.set_comment(description);
1073+
dest.add(goto_programt::make_assertion(false_exprt(), annotated_location));
10761074
// we ignore any LHS
10771075
}
10781076
else if(identifier==CPROVER_PREFIX "fence")

‎src/goto-programs/goto_inline_class.cpp

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -47,9 +47,8 @@ void goto_inlinet::parameter_assignments(
4747
// this is the type the n-th argument should have
4848
const typet &parameter_type = symbol.type;
4949

50-
goto_programt::targett decl =
51-
dest.add(goto_programt::make_decl(symbol.symbol_expr(), source_location));
52-
decl->code_nonconst().add_source_location() = source_location;
50+
dest.add(goto_programt::make_decl(
51+
code_declt{symbol.symbol_expr(), source_location}, source_location));
5352

5453
// this is the actual parameter
5554
exprt actual;
@@ -140,9 +139,8 @@ void goto_inlinet::parameter_destruction(
140139
{
141140
const symbolt &symbol=ns.lookup(identifier);
142141

143-
goto_programt::targett dead = dest.add(
144-
goto_programt::make_dead(symbol.symbol_expr(), source_location));
145-
dead->code_nonconst().add_source_location() = source_location;
142+
dest.add(goto_programt::make_dead(
143+
code_deadt{symbol.symbol_expr(), source_location}, source_location));
146144
}
147145
}
148146
}

‎src/goto-programs/string_abstraction.cpp

Lines changed: 47 additions & 66 deletions
Original file line numberDiff line numberDiff line change
@@ -300,10 +300,9 @@ void string_abstractiont::make_decl_and_def(goto_programt &dest,
300300
{
301301
const symbolt &symbol=ns.lookup(identifier);
302302
symbol_exprt sym_expr=symbol.symbol_expr();
303+
code_declt decl{sym_expr, ref_instr->source_location()};
303304

304-
goto_programt::targett decl1 =
305-
dest.add(goto_programt::make_decl(sym_expr, ref_instr->source_location()));
306-
decl1->code_nonconst().add_source_location() = ref_instr->source_location();
305+
dest.add(goto_programt::make_decl(decl, ref_instr->source_location()));
307306

308307
exprt val=symbol.value;
309308
// initialize pointers with suitable objects
@@ -316,11 +315,9 @@ void string_abstractiont::make_decl_and_def(goto_programt &dest,
316315
// may still be nil (structs, then assignments have been done already)
317316
if(val.is_not_nil())
318317
{
319-
goto_programt::targett assignment1 =
320-
dest.add(goto_programt::make_assignment(
321-
code_assignt(sym_expr, val), ref_instr->source_location()));
322-
assignment1->code_nonconst().add_source_location() =
323-
ref_instr->source_location();
318+
code_assignt assignment{sym_expr, val, ref_instr->source_location()};
319+
dest.add(
320+
goto_programt::make_assignment(assignment, ref_instr->source_location()));
324321
}
325322
}
326323

@@ -376,11 +373,9 @@ exprt string_abstractiont::make_val_or_dummy_rec(goto_programt &dest,
376373

377374
member_exprt member(symbol.symbol_expr(), it2->get_name(), it2->type());
378375

379-
goto_programt::targett assignment1 =
380-
dest.add(goto_programt::make_assignment(
381-
code_assignt(member, sym_expr), ref_instr->source_location()));
382-
assignment1->code_nonconst().add_source_location() =
383-
ref_instr->source_location();
376+
code_assignt assignment{member, sym_expr, ref_instr->source_location()};
377+
dest.add(goto_programt::make_assignment(
378+
code_assignt(member, sym_expr), ref_instr->source_location()));
384379
}
385380

386381
++seen;
@@ -423,9 +418,8 @@ symbol_exprt string_abstractiont::add_dummy_symbol_and_value(
423418
symbol_exprt sym_expr=new_symbol.symbol_expr();
424419

425420
// make sure it is declared before the recursive call
426-
goto_programt::targett decl =
427-
dest.add(goto_programt::make_decl(sym_expr, ref_instr->source_location()));
428-
decl->code_nonconst().add_source_location() = ref_instr->source_location();
421+
code_declt decl{sym_expr, ref_instr->source_location()};
422+
dest.add(goto_programt::make_decl(decl, ref_instr->source_location()));
429423

430424
// set the value - may be nil
431425
if(
@@ -448,12 +442,10 @@ symbol_exprt string_abstractiont::add_dummy_symbol_and_value(
448442

449443
if(new_symbol.value.is_not_nil())
450444
{
451-
goto_programt::targett assignment1 =
452-
dest.add(goto_programt::make_assignment(
453-
code_assignt(sym_expr, new_symbol.value),
454-
ref_instr->source_location()));
455-
assignment1->code_nonconst().add_source_location() =
456-
ref_instr->source_location();
445+
code_assignt assignment{
446+
sym_expr, new_symbol.value, ref_instr->source_location()};
447+
dest.add(
448+
goto_programt::make_assignment(assignment, ref_instr->source_location()));
457449
}
458450

459451
symbol_table.insert(std::move(new_symbol));
@@ -1026,8 +1018,12 @@ void string_abstractiont::build_new_symbol(const symbolt &symbol,
10261018
if(symbol.is_static_lifetime)
10271019
{
10281020
goto_programt::targett dummy_loc =
1029-
initialization.add(goto_programt::instructiont());
1030-
dummy_loc->source_location_nonconst() = symbol.location;
1021+
initialization.add(goto_programt::instructiont{
1022+
codet{ID_nil},
1023+
symbol.location,
1024+
goto_program_instruction_typet::NO_INSTRUCTION_TYPE,
1025+
{},
1026+
{}});
10311027
make_decl_and_def(initialization, dummy_loc, identifier, symbol.name);
10321028
initialization.instructions.erase(dummy_loc);
10331029
}
@@ -1128,11 +1124,9 @@ goto_programt::targett string_abstractiont::abstract_pointer_assign(
11281124

11291125
if(lhs.type().id()==ID_pointer && !unknown)
11301126
{
1131-
goto_programt::instructiont assignment;
1132-
assignment = goto_programt::make_assignment(
1133-
code_assignt(new_lhs, new_rhs), target->source_location());
1134-
assignment.code_nonconst().add_source_location() =
1135-
target->source_location();
1127+
goto_programt::instructiont assignment = goto_programt::make_assignment(
1128+
code_assignt(new_lhs, new_rhs, target->source_location()),
1129+
target->source_location());
11361130
dest.insert_before_swap(target, assignment);
11371131

11381132
return std::next(target);
@@ -1220,18 +1214,14 @@ goto_programt::targett string_abstractiont::char_assign(
12201214
i1.is_not_nil(),
12211215
"failed to create is_zero-component for the left-hand-side");
12221216

1223-
goto_programt::targett assignment1 = tmp.add(goto_programt::make_assignment(
1224-
code_assignt(i1, from_integer(1, i1.type())), target->source_location()));
1225-
assignment1->code_nonconst().add_source_location() =
1226-
target->source_location();
1217+
tmp.add(goto_programt::make_assignment(
1218+
code_assignt(i1, from_integer(1, i1.type()), target->source_location()),
1219+
target->source_location()));
12271220

1228-
goto_programt::targett assignment2 = tmp.add(goto_programt::make_assignment(
1229-
code_assignt(lhs, rhs), target->source_location()));
1230-
assignment2->code_nonconst().add_source_location() =
1231-
target->source_location();
1232-
1233-
move_lhs_arithmetic(
1234-
assignment2->code_nonconst().op0(), assignment2->code_nonconst().op1());
1221+
code_assignt assignment{lhs, rhs, target->source_location()};
1222+
move_lhs_arithmetic(assignment.lhs(), assignment.rhs());
1223+
tmp.add(
1224+
goto_programt::make_assignment(assignment, target->source_location()));
12351225

12361226
dest.insert_before_swap(target, tmp);
12371227
++target;
@@ -1326,32 +1316,23 @@ goto_programt::targett string_abstractiont::value_assignments_string_struct(
13261316
// copy all the values
13271317
goto_programt tmp;
13281318

1329-
{
1330-
goto_programt::targett assignment = tmp.add(goto_programt::make_assignment(
1331-
member(lhs, whatt::IS_ZERO),
1332-
member(rhs, whatt::IS_ZERO),
1333-
target->source_location()));
1334-
assignment->code_nonconst().add_source_location() =
1335-
target->source_location();
1336-
}
1337-
1338-
{
1339-
goto_programt::targett assignment = tmp.add(goto_programt::make_assignment(
1340-
member(lhs, whatt::LENGTH),
1341-
member(rhs, whatt::LENGTH),
1342-
target->source_location()));
1343-
assignment->code_nonconst().add_source_location() =
1344-
target->source_location();
1345-
}
1346-
1347-
{
1348-
goto_programt::targett assignment = tmp.add(goto_programt::make_assignment(
1349-
member(lhs, whatt::SIZE),
1350-
member(rhs, whatt::SIZE),
1351-
target->source_location()));
1352-
assignment->code_nonconst().add_source_location() =
1353-
target->source_location();
1354-
}
1319+
tmp.add(goto_programt::make_assignment(
1320+
code_assignt{member(lhs, whatt::IS_ZERO),
1321+
member(rhs, whatt::IS_ZERO),
1322+
target->source_location()},
1323+
target->source_location()));
1324+
1325+
tmp.add(goto_programt::make_assignment(
1326+
code_assignt{member(lhs, whatt::LENGTH),
1327+
member(rhs, whatt::LENGTH),
1328+
target->source_location()},
1329+
target->source_location()));
1330+
1331+
tmp.add(goto_programt::make_assignment(
1332+
code_assignt{member(lhs, whatt::SIZE),
1333+
member(rhs, whatt::SIZE),
1334+
target->source_location()},
1335+
target->source_location()));
13551336

13561337
goto_programt::targett last=target;
13571338
++last;

0 commit comments

Comments
 (0)