Skip to content

Commit 17b87d3

Browse files
Do not make replace_nondet public
1 parent 29c1ca1 commit 17b87d3

File tree

3 files changed

+14
-17
lines changed

3 files changed

+14
-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: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -135,6 +135,20 @@ 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+
Forall_operands(it, expr)
149+
replace_nondet(*it, nondet_count);
150+
}
151+
138152
void goto_symext::clean_expr(
139153
exprt &expr,
140154
statet &state,

0 commit comments

Comments
 (0)