Skip to content

Commit 5f5ba22

Browse files
Do not make replace_nondet public
1 parent 58d6122 commit 5f5ba22

File tree

3 files changed

+16
-17
lines changed

3 files changed

+16
-17
lines changed

src/goto-symex/goto_symex.cpp

Lines changed: 0 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -28,18 +28,3 @@ nondet_symbol_exprt build_symex_nondet(typet &type, unsigned &nondet_count)
2828
nondet_symbol_exprt new_expr(identifier, type);
2929
return new_expr;
3030
}
31-
32-
void replace_nondet(exprt &expr, unsigned &nondet_count)
33-
{
34-
if(expr.id()==ID_side_effect &&
35-
expr.get(ID_statement)==ID_nondet)
36-
{
37-
nondet_symbol_exprt new_expr =
38-
build_symex_nondet(expr.type(), nondet_count);
39-
new_expr.add_source_location()=expr.source_location();
40-
expr.swap(new_expr);
41-
}
42-
else
43-
Forall_operands(it, expr)
44-
replace_nondet(*it, nondet_count);
45-
}

src/goto-symex/goto_symex.h

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -451,8 +451,6 @@ class goto_symext
451451

452452
nondet_symbol_exprt build_symex_nondet(typet &type, unsigned &nondet_count);
453453

454-
void replace_nondet(exprt &, unsigned &);
455-
456454
void symex_transition(goto_symext::statet &state);
457455

458456
void symex_transition(

src/goto-symex/symex_clean_expr.cpp

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -135,6 +135,22 @@ static void adjust_byte_extract_rec(exprt &expr, const namespacet &ns)
135135
}
136136
}
137137

138+
static void replace_nondet(exprt &expr, unsigned &nondet_count)
139+
{
140+
if(expr.id() == ID_side_effect && expr.get(ID_statement) == ID_nondet)
141+
{
142+
nondet_symbol_exprt new_expr =
143+
build_symex_nondet(expr.type(), nondet_count);
144+
new_expr.add_source_location() = expr.source_location();
145+
expr.swap(new_expr);
146+
}
147+
else
148+
{
149+
Forall_operands(it, expr)
150+
replace_nondet(*it, nondet_count);
151+
}
152+
}
153+
138154
void goto_symext::clean_expr(
139155
exprt &expr,
140156
statet &state,

0 commit comments

Comments
 (0)