Skip to content

Commit 5f6e6ae

Browse files
author
Daniel Kroening
committed
bugfix: set assignment type for actual parameters correctly
1 parent 1893fdb commit 5f6e6ae

File tree

1 file changed

+15
-1
lines changed

1 file changed

+15
-1
lines changed

src/goto-symex/symex_function_call.cpp

Lines changed: 15 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -125,7 +125,21 @@ void goto_symext::parameter_assignments(
125125
}
126126
}
127127

128-
symex_assign(state, code_assignt(lhs, rhs));
128+
assignment_typet assignment_type;
129+
130+
// We hide if we are in a hidden function.
131+
if(state.top().hidden_function)
132+
assignment_type =
133+
symex_targett::assignment_typet::HIDDEN_ACTUAL_PARAMETER;
134+
else
135+
assignment_type =
136+
symex_targett::assignment_typet::VISIBLE_ACTUAL_PARAMETER;
137+
138+
clean_expr(lhs, state, true);
139+
clean_expr(rhs, state, false);
140+
141+
guardt guard;
142+
symex_assign_rec(state, lhs, nil_exprt(), rhs, guard, assignment_type);
129143
}
130144

131145
if(it1!=arguments.end())

0 commit comments

Comments
 (0)