From 302d06ab862a6fe4239532c88208d5771ecb8b1b Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 24 Dec 2020 00:10:45 +0000
Subject: [PATCH] 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.
---
 regression/cbmc/KnR1/main.c     |  8 ++++++++
 regression/cbmc/KnR1/test.desc  |  9 +++++++++
 src/ansi-c/c_typecheck_expr.cpp | 10 ++++++----
 3 files changed, 23 insertions(+), 4 deletions(-)
 create mode 100644 regression/cbmc/KnR1/main.c
 create mode 100644 regression/cbmc/KnR1/test.desc

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())
   {