Skip to content

Commit 9de1a02

Browse files
authored
Merge pull request #3677 from tautschnig/vs-shadow-goto-programs
Avoid shadowing in directory goto-programs [blocks: #2310]
2 parents c8724c8 + ae29373 commit 9de1a02

File tree

6 files changed

+33
-38
lines changed

6 files changed

+33
-38
lines changed

src/goto-programs/goto_inline.cpp

Lines changed: 10 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -55,9 +55,9 @@ void goto_inline(
5555
if(it==goto_functions.function_map.end())
5656
return;
5757

58-
goto_functiont &goto_function=it->second;
58+
goto_functiont &entry_function = it->second;
5959
DATA_INVARIANT(
60-
goto_function.body_available(),
60+
entry_function.body_available(),
6161
"body of entry point function must be available");
6262

6363
// gather all calls
@@ -86,7 +86,7 @@ void goto_inline(
8686
}
8787

8888
goto_inline.goto_inline(
89-
goto_functionst::entry_point(), goto_function, inline_map, true);
89+
goto_functionst::entry_point(), entry_function, inline_map, true);
9090

9191
// clean up
9292
Forall_goto_functions(f_it, goto_functions)
@@ -180,24 +180,23 @@ void goto_partial_inline(
180180
const symbol_exprt &symbol_expr=to_symbol_expr(function_expr);
181181
const irep_idt id=symbol_expr.get_identifier();
182182

183-
goto_functionst::function_mapt::const_iterator f_it=
183+
goto_functionst::function_mapt::const_iterator called_it =
184184
goto_functions.function_map.find(id);
185185

186-
if(f_it==goto_functions.function_map.end())
186+
if(called_it == goto_functions.function_map.end())
187187
// Function not loaded, can't check size
188188
continue;
189189

190190
// called function
191-
const goto_functiont &goto_function=f_it->second;
191+
const goto_functiont &called_function = called_it->second;
192192

193-
if(!goto_function.body_available())
193+
if(!called_function.body_available())
194194
// The bodies of functions that don't have bodies can't be inlined.
195195
continue;
196196

197-
const goto_programt &goto_program=goto_function.body;
198-
199-
if(goto_function.is_inlined() ||
200-
goto_program.instructions.size()<=smallfunc_limit)
197+
if(
198+
called_function.is_inlined() ||
199+
called_function.body.instructions.size() <= smallfunc_limit)
201200
{
202201
PRECONDITION(i_it->is_function_call());
203202

src/goto-programs/instrument_preconditions.cpp

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -78,11 +78,9 @@ replace_symbolt actuals_replace_map(
7878
if(p.get_identifier()!=irep_idt() &&
7979
arguments.size()>count)
8080
{
81-
exprt a=arguments[count];
82-
if(a.type()!=p.type())
83-
a=typecast_exprt(a, p.type());
84-
symbol_exprt s(p.get_identifier(), p.type());
85-
result.insert(s, a);
81+
const exprt a =
82+
typecast_exprt::conditional_cast(arguments[count], p.type());
83+
result.insert(symbol_exprt(p.get_identifier(), p.type()), a);
8684
}
8785
count++;
8886
}

src/goto-programs/interpreter.cpp

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -611,21 +611,22 @@ exprt interpretert::get_value(
611611
// We want the symbol pointed to
612612
mp_integer address = rhs[numeric_cast_v<std::size_t>(offset)];
613613
irep_idt identifier=address_to_identifier(address);
614-
mp_integer offset=address_to_offset(address);
615-
const typet type=get_type(identifier);
616-
const symbol_exprt symbol_expr(identifier, type);
614+
mp_integer offset_from_address = address_to_offset(address);
615+
const typet type_from_identifier = get_type(identifier);
616+
const symbol_exprt symbol_expr(identifier, type_from_identifier);
617617

618-
if(offset==0)
618+
if(offset_from_address == 0)
619619
return address_of_exprt(symbol_expr);
620620

621-
if(ns.follow(type).id()==ID_struct)
621+
if(ns.follow(type_from_identifier).id() == ID_struct)
622622
{
623-
const auto c=get_component(identifier, offset);
623+
const auto c = get_component(identifier, offset_from_address);
624624
member_exprt member_expr(symbol_expr, c);
625625
return address_of_exprt(member_expr);
626626
}
627627

628-
return index_exprt(symbol_expr, from_integer(offset, integer_typet()));
628+
return index_exprt(
629+
symbol_expr, from_integer(offset_from_address, integer_typet()));
629630
}
630631

631632
error() << "interpreter: invalid pointer "

src/goto-programs/json_goto_trace.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -138,9 +138,9 @@ void convert_decl(
138138
type_string = from_type(ns, identifier, symbol->type);
139139

140140
json_assignment["mode"] = json_stringt(symbol->mode);
141-
exprt simplified = simplify_expr(step.full_lhs_value, ns);
141+
const exprt simplified_expr = simplify_expr(step.full_lhs_value, ns);
142142

143-
full_lhs_value = json(simplified, ns, symbol->mode);
143+
full_lhs_value = json(simplified_expr, ns, symbol->mode);
144144
}
145145
else
146146
{

src/goto-programs/replace_calls.cpp

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -103,13 +103,12 @@ void replace_callst::operator()(
103103
const code_assignt &ca = to_code_assign(next_it->code);
104104
const exprt &rhs = ca.rhs();
105105

106-
if(rhs.id() == ID_symbol)
107-
{
108-
const symbol_exprt &se = to_symbol_expr(rhs);
109-
INVARIANT(
110-
!has_suffix(id2string(se.get_identifier()), RETURN_VALUE_SUFFIX),
111-
"returns must not be removed before replacing calls");
112-
}
106+
INVARIANT(
107+
rhs.id() != ID_symbol ||
108+
!has_suffix(
109+
id2string(to_symbol_expr(rhs).get_identifier()),
110+
RETURN_VALUE_SUFFIX),
111+
"returns must not be removed before replacing calls");
113112
}
114113

115114
// Finally modify the call

src/goto-programs/string_instrumentation.cpp

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -453,9 +453,8 @@ void string_instrumentationt::do_format_string_read(
453453
format_ass->make_assertion(is_zero_string(arguments[1]));
454454
format_ass->source_location=target->source_location;
455455
format_ass->source_location.set_property_class("string");
456-
std::string comment("zero-termination of format string of ");
457-
comment += function_name;
458-
format_ass->source_location.set_comment(comment);
456+
format_ass->source_location.set_comment(
457+
"zero-termination of format string of " + function_name);
459458

460459
for(std::size_t i=2; i<arguments.size(); i++)
461460
{
@@ -468,9 +467,8 @@ void string_instrumentationt::do_format_string_read(
468467
goto_programt::targett assertion=dest.add_instruction();
469468
assertion->source_location=target->source_location;
470469
assertion->source_location.set_property_class("string");
471-
std::string comment("zero-termination of string argument of ");
472-
comment += function_name;
473-
assertion->source_location.set_comment(comment);
470+
assertion->source_location.set_comment(
471+
"zero-termination of string argument of " + function_name);
474472

475473
exprt temp(arg);
476474

0 commit comments

Comments
 (0)