Skip to content

Commit 5a25e47

Browse files
Infer hidden field in SSA_assignment_stept
We can deduce it from the assignment type rather than having to give it to the constructor.
1 parent f153ab6 commit 5a25e47

File tree

3 files changed

+7
-8
lines changed

3 files changed

+7
-8
lines changed

src/goto-symex/ssa_step.cpp

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -222,8 +222,7 @@ SSA_assignment_stept::SSA_assignment_stept(
222222
exprt _original_full_lhs,
223223
exprt _ssa_rhs,
224224
exprt _cond_expr,
225-
symex_targett::assignment_typet _assignment_type,
226-
bool _hidden)
225+
symex_targett::assignment_typet _assignment_type)
227226
: SSA_stept(source, goto_trace_stept::typet::ASSIGNMENT)
228227
{
229228
guard = std::move(_guard);
@@ -233,5 +232,8 @@ SSA_assignment_stept::SSA_assignment_stept(
233232
ssa_rhs = std::move(_ssa_rhs);
234233
assignment_type = _assignment_type;
235234
cond_expr = std::move(_cond_expr);
236-
hidden = _hidden;
235+
hidden =
236+
assignment_type != symex_targett::assignment_typet::STATE &&
237+
assignment_type !=
238+
symex_targett::assignment_typet::VISIBLE_ACTUAL_PARAMETER;
237239
}

src/goto-symex/ssa_step.h

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -206,8 +206,7 @@ class SSA_assignment_stept : public SSA_stept
206206
exprt original_full_lhs,
207207
exprt ssa_rhs,
208208
exprt cond_expr,
209-
symex_targett::assignment_typet assignment_type,
210-
bool hidden);
209+
symex_targett::assignment_typet assignment_type);
211210
};
212211

213212
#endif // CPROVER_GOTO_SYMEX_SSA_STEP_H

src/goto-symex/symex_target_equation.cpp

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -122,9 +122,7 @@ void symex_target_equationt::assignment(
122122
original_full_lhs,
123123
ssa_rhs,
124124
equal_exprt(ssa_lhs, ssa_rhs),
125-
assignment_type,
126-
assignment_type != assignment_typet::STATE &&
127-
assignment_type != assignment_typet::VISIBLE_ACTUAL_PARAMETER});
125+
assignment_type});
128126

129127
merge_ireps(SSA_steps.back());
130128
}

0 commit comments

Comments
 (0)