Merge pull request #5692 from tautschnig/knr-nondet

C front-end/KnR: generate nondet for missing arguments

Author: tautschnig

regression/cbmc/KnR1/main.c

@@ -0,0 +1,8 @@
+void a(b)
+{
+  __CPROVER_assert(0, "");
+}
+int main()
+{
+  a();
+}

regression/cbmc/KnR1/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+Invariant check failed

src/ansi-c/c_typecheck_expr.cpp

@@ -3763,10 +3763,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())
   {