Skip to content

Commit d20b124

Browse files
author
Daniel Kroening
committed
bugfix: set assignment type for actual parameters correctly
1 parent 31060e1 commit d20b124

File tree

2 files changed

+16
-2
lines changed

2 files changed

+16
-2
lines changed

regression/cbmc/compact-trace/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,6 @@ activate-multi-line-match
55
^EXIT=10$
66
^SIGNAL=0$
77
^↳ main\.c:10 main\(\)\n 12: x=1 .*$
8-
^↳ main.c:13 bar\(0\)\n 13: bar_a=0 .*\n 5: x=2 .*\n 6: x=3 .*$
8+
^↳ main\.c:13 bar\(0\)\n 5: x=2 .*\n 6: x=3 .*$
99
--
1010
^warning: ignoring

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)