Skip to content

Commit 302d06a

Browse files
committed
C front-end/KnR: generate nondet for missing arguments
The back-end does not know how to handle `nil`, and symex would also generate nondet in such cases, so do the same in the front-end.
1 parent d932d6f commit 302d06a

File tree

3 files changed

+23
-4
lines changed

3 files changed

+23
-4
lines changed

regression/cbmc/KnR1/main.c

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
void a(b)
2+
{
3+
__CPROVER_assert(0, "");
4+
}
5+
int main()
6+
{
7+
a();
8+
}

regression/cbmc/KnR1/test.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
^warning: ignoring
9+
Invariant check failed

src/ansi-c/c_typecheck_expr.cpp

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3698,10 +3698,12 @@ void c_typecheck_baset::typecheck_function_call_arguments(
36983698
else if(code_type.is_KnR())
36993699
{
37003700
// We are generous on KnR; any number is ok.
3701-
// We will in missing ones with "NIL".
3702-
3703-
while(parameters.size() > arguments.size())
3704-
arguments.push_back(nil_exprt());
3701+
// We will fill in missing ones with "nondet".
3702+
for(std::size_t i = arguments.size(); i < parameters.size(); ++i)
3703+
{
3704+
arguments.push_back(
3705+
side_effect_expr_nondett{parameters[i].type(), expr.source_location()});
3706+
}
37053707
}
37063708
else if(code_type.has_ellipsis())
37073709
{

0 commit comments

Comments
 (0)