Skip to content

Commit 1653959

Browse files
Change signature of the public rename_level0
This reflects betters how we expect it to be used, and remove some unused code. Not that the old version of the signature has to be kept as it is used for rename_type.
1 parent 6758d92 commit 1653959

File tree

3 files changed

+23
-14
lines changed

3 files changed

+23
-14
lines changed

src/goto-symex/goto_symex_state.cpp

Lines changed: 20 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -280,14 +280,12 @@ static void set_l2_indices(
280280
ssa_expr.set_level_2(level2.current_count(ssa_expr.get_identifier()));
281281
}
282282

283-
void goto_symex_statet::rename_level0(exprt &expr, const namespacet &ns)
283+
exprt goto_symex_statet::rename_level0(exprt expr, const namespacet &ns)
284284
{
285285
// rename all the symbols with their last known value
286286
if(auto ssa = expr_try_dynamic_cast<ssa_exprt>(expr))
287287
{
288-
set_l0_indices(level0, *ssa, source.thread_nr, ns);
289-
rename(expr.type(), ssa->get_identifier(), ns, L0);
290-
ssa->update_type();
288+
return rename_level0(*ssa, ns);
291289
}
292290
else if(expr.id() == ID_symbol)
293291
{
@@ -296,16 +294,17 @@ void goto_symex_statet::rename_level0(exprt &expr, const namespacet &ns)
296294
{
297295
rename(expr.type(), to_symbol_expr(expr).get_identifier(), ns, L0);
298296

299-
return;
297+
return expr;
300298
}
301299

302300
expr = ssa_exprt(expr);
303-
rename_level0(expr, ns);
301+
return rename_level0(expr, ns);
304302
}
305303
else if(auto address_of_expr = expr_try_dynamic_cast<address_of_exprt>(expr))
306304
{
307305
rename_address(address_of_expr->object(), ns, L0);
308306
to_pointer_type(expr.type()).subtype() = address_of_expr->object().type();
307+
return expr;
309308
}
310309
else
311310
{
@@ -317,9 +316,20 @@ void goto_symex_statet::rename_level0(exprt &expr, const namespacet &ns)
317316
rename_level0(op, ns);
318317

319318
fix_type(expr);
319+
return expr;
320320
}
321321
}
322322

323+
ssa_exprt
324+
goto_symex_statet::rename_level0(const symbol_exprt &expr, const namespacet &ns)
325+
{
326+
ssa_exprt ssa{expr};
327+
set_l0_indices(level0, ssa, source.thread_nr, ns);
328+
rename(ssa.type(), ssa.get_identifier(), ns, L0);
329+
ssa.update_type();
330+
return ssa;
331+
}
332+
323333
void goto_symex_statet::rename_level1(exprt &expr, const namespacet &ns)
324334
{
325335
// rename all the symbols with their last known value
@@ -612,10 +622,9 @@ void goto_symex_statet::rename_address(
612622
const namespacet &ns,
613623
levelt level)
614624
{
625+
PRECONDITION(level != L0);
615626
auto rename_expr = [&](exprt &e) {
616-
if(level == L0)
617-
rename_level0(e, ns);
618-
else if(level == L1)
627+
if(level == L1)
619628
rename_level1(e, ns);
620629
else
621630
rename_level2(e, ns);
@@ -718,8 +727,8 @@ void goto_symex_statet::rename(
718727
{
719728
auto rename_expr = [&](exprt &e) {
720729
if(level == L0)
721-
rename_level0(e, ns);
722-
else if(level == L1)
730+
e = rename_level0(std::move(e), ns);
731+
if(level == L1)
723732
rename_level1(e, ns);
724733
else
725734
rename_level2(e, ns);

src/goto-symex/goto_symex_state.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -71,7 +71,7 @@ class goto_symex_statet final
7171
enum levelt { L0=0, L1=1, L2=2 };
7272

7373
// performs renaming _up to_ the given level
74-
void rename_level0(exprt &expr, const namespacet &ns);
74+
ssa_exprt rename_level0(const symbol_exprt &expr, const namespacet &ns);
7575
void rename_level1(exprt &expr, const namespacet &ns);
7676
void rename_level2(exprt &expr, const namespacet &ns);
7777
void rename(
@@ -92,6 +92,7 @@ class goto_symex_statet final
9292
void get_original_name(exprt &expr) const;
9393
void get_original_name(typet &type) const;
9494
protected:
95+
exprt rename_level0(exprt expr, const namespacet &ns);
9596
void rename_address(exprt &expr, const namespacet &ns, levelt level);
9697

9798
// this maps L1 names to (L2) types

src/goto-symex/symex_function_call.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -399,8 +399,7 @@ void goto_symext::locality(
399399
it++)
400400
{
401401
// get L0 name
402-
ssa_exprt ssa(ns.lookup(*it).symbol_expr());
403-
state.rename_level0(ssa, ns);
402+
ssa_exprt ssa = state.rename_level0(ns.lookup(*it).symbol_expr(), ns);
404403
const irep_idt l0_name=ssa.get_identifier();
405404

406405
// save old L1 name for popping the frame

0 commit comments

Comments
 (0)