test for signature conflict with undeclared function

Author: Daniel Kroening

regression/cbmc/return6/f_def.c

@@ -0,0 +1,4 @@
+unsigned f()
+{
+  return 0x34;
+}

regression/cbmc/return6/main.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+
+// Do not declare f().
+// This is invalid from C99 upwards, but kind of ok before.
+
+int main()
+{
+  int return_value;
+  return_value=f();
+  assert(return_value==0x34);
+}

regression/cbmc/return6/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+f_def.c
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring