diff --git a/regression/cbmc/KnR1/main.c b/regression/cbmc/KnR1/main.c new file mode 100644 index 00000000000..1020dd10be6 --- /dev/null +++ b/regression/cbmc/KnR1/main.c @@ -0,0 +1,8 @@ +void a(b) +{ + __CPROVER_assert(0, ""); +} +int main() +{ + a(); +} diff --git a/regression/cbmc/KnR1/test.desc b/regression/cbmc/KnR1/test.desc new file mode 100644 index 00000000000..574296748f3 --- /dev/null +++ b/regression/cbmc/KnR1/test.desc @@ -0,0 +1,9 @@ +CORE +main.c + +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring +Invariant check failed diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index cd41c414c86..4ab3ffe7601 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -3698,10 +3698,12 @@ void c_typecheck_baset::typecheck_function_call_arguments( else if(code_type.is_KnR()) { // We are generous on KnR; any number is ok. - // We will in missing ones with "NIL". - - while(parameters.size() > arguments.size()) - arguments.push_back(nil_exprt()); + // We will fill in missing ones with "nondet". + for(std::size_t i = arguments.size(); i < parameters.size(); ++i) + { + arguments.push_back( + side_effect_expr_nondett{parameters[i].type(), expr.source_location()}); + } } else if(code_type.has_ellipsis()) {