C front-end: tolerate type differences with asm renaming

regression/ansi-c/asm4/main.c

@@ -0,0 +1,26 @@
+// from Fedora's glibc
+struct dirent
+{
+  int dummy;
+};
+
+struct dirent64
+{
+  int dummy;
+};
+
+#ifdef __GNUC__
+extern struct dirent *readdir(void *__dirp) __asm__(
+  ""
+  "readdir64");
+extern struct dirent64 *readdir64(void *__dirp);
+#endif
+
+int main()
+{
+#ifdef __GNUC__
+  int x;
+  (void)readdir(&x);
+#endif
+  return 0;
+}

regression/ansi-c/asm4/test.desc

@@ -0,0 +1,8 @@
+CORE test-c++-front-end
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

regression/cbmc-library/sscanf-01/main.c

@@ -3,7 +3,8 @@
 
 int main()
 {
-  sscanf();
-  assert(0);
+  char dest[10];
+  int result = sscanf("hello", "%s", dest);
+  assert(result == 1);
   return 0;
 }

regression/cbmc-library/sscanf-01/test.desc

@@ -1,8 +1,10 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
-^EXIT=0$
+
+^\[main.assertion.1\] line 8 assertion result == 1: FAILURE$
+^\*\* 1 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

regression/cbmc-library/vfscanf-01/main.c

@@ -1,9 +1,20 @@
 #include <assert.h>
+#include <stdarg.h>
 #include <stdio.h>
 
+int xscanf(const char *format, ...)
+{
+  va_list list;
+  va_start(list, format);
+  int result = vfscanf(stdin, format, list);
+  va_end(list);
+  return result;
+}
+
 int main()
 {
-  vfscanf();
-  assert(0);
+  char dest[10];
+  int result = xscanf("%s", dest);
+  assert(result == 1);
   return 0;
 }

regression/cbmc-library/vfscanf-01/test.desc

@@ -1,8 +1,10 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
-^EXIT=0$
+
+^\[main.assertion.1\] line 18 assertion result == 1: FAILURE$
+^\*\* 1 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

regression/cbmc-library/vscanf-01/main.c

@@ -1,9 +1,20 @@
 #include <assert.h>
+#include <stdarg.h>
 #include <stdio.h>
 
+int xscanf(const char *format, ...)
+{
+  va_list list;
+  va_start(list, format);
+  int result = vscanf(format, list);
+  va_end(list);
+  return result;
+}
+
 int main()
 {
-  vscanf();
-  assert(0);
+  char dest[10];
+  int result = xscanf("%s", dest);
+  assert(result == 1);
   return 0;
 }

regression/cbmc-library/vscanf-01/test.desc

@@ -1,8 +1,10 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
-^EXIT=0$
+
+^\[main.assertion.1\] line 18 assertion result == 1: FAILURE$
+^\*\* 1 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

regression/cbmc-library/vsscanf-01/main.c

@@ -1,9 +1,20 @@
 #include <assert.h>
+#include <stdarg.h>
 #include <stdio.h>
 
+int xscanf(const char *format, ...)
+{
+  va_list list;
+  va_start(list, format);
+  int result = vsscanf("hello", format, list);
+  va_end(list);
+  return result;
+}
+
 int main()
 {
-  vsscanf();
-  assert(0);
+  char dest[10];
+  int result = xscanf("%s", dest);
+  assert(result == 1);
   return 0;
 }

regression/cbmc-library/vsscanf-01/test.desc

@@ -1,8 +1,10 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
-^EXIT=0$
+
+^\[main.assertion.1\] line 18 assertion result == 1: FAILURE$
+^\*\* 1 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

src/ansi-c/c_typecheck_base.cpp

@@ -668,6 +668,10 @@ void c_typecheck_baset::apply_asm_label(
   {
     symbol.name=asm_label;
     symbol.base_name=asm_label;
+    // asm renaming may be combined with varied return types - make sure the
+    // actual definition sets the final type
+    if(symbol.type.id() == ID_code)
+      symbol.type.set(ID_C_incomplete, true);
   }
 
   if(symbol.name!=orig_name)