Merge pull request #6547 from tautschnig/pointer-parameter-type-conflict

Fix linking in case of function type conflict

Author: kroening

regression/ansi-c/undeclared_function/fileB.c

@@ -1,4 +1,7 @@
-#include <stdlib.h>
+void *malloc(__CPROVER_size_t s)
+{
+  return (void *)0 + s;
+}
 
 int f()
 {

regression/ansi-c/undeclared_function/undeclared_function1.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE gcc-only
 fileA.c
 fileB.c --validate-goto-model
 ^EXIT=0$

regression/cbmc/incomplete-structs/test.desc

@@ -0,0 +1,13 @@
+CORE
+typesmain.c
+types1.c types2.c types3.c
+reason for conflict at \*#this.u: number of members is different \(3/0\)
+reason for conflict at \*#this.u: number of members is different \(0/3\)
+struct U   \(incomplete\)
+warning: pointer parameter types differ between declaration and definition "bar"
+warning: pointer parameter types differ between declaration and definition "foo"
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc/incomplete-structs/types1.c

@@ -0,0 +1,9 @@
+struct S
+{
+  int s;
+} s_object;
+
+int foobar()
+{
+  return s_object.s;
+}

regression/cbmc/incomplete-structs/types2.c

@@ -0,0 +1,16 @@
+struct S
+{
+  struct T *t;
+  struct U *u;
+};
+
+struct U
+{
+  struct S *s;
+  int j;
+};
+
+int bar(struct S *s)
+{
+  return s->u->j;
+}

regression/cbmc/incomplete-structs/types3.c

@@ -0,0 +1,17 @@
+struct T
+{
+  int i;
+};
+
+struct S
+{
+  struct T *t;
+  struct U *u;
+};
+
+int bar(struct S *);
+
+int foo(struct S *s)
+{
+  return bar(s) + s->t->i;
+}

regression/cbmc/incomplete-structs/typesmain.c

@@ -0,0 +1,29 @@
+#include <assert.h>
+
+struct T
+{
+  int i;
+};
+
+struct U
+{
+  struct S *s;
+  int j;
+};
+
+struct S
+{
+  struct T *t;
+  struct U *u;
+};
+
+int foo(struct S *s);
+
+int main()
+{
+  struct T t = {10};
+  struct U u = {0, 32};
+  struct S s = {&t, &u};
+  int res = foo(&s);
+  assert(res == 42);
+}

regression/cbmc/return6/test.desc

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

regression/linking-goto-binaries/chain.sh

@@ -21,4 +21,4 @@ else
   $goto_cc "${main}.gb" "${next}.gb" -o "final.gb"
 fi
 
-$cbmc "final.gb"
+$cbmc --validate-goto-model "final.gb"

regression/linking-goto-binaries/type_conflicts/Linking7-main.c

@@ -0,0 +1,19 @@
+struct S
+{
+  void *a;
+  void *b;
+};
+
+typedef void (*fptr)(struct S);
+
+extern void foo(struct S s);
+
+fptr A[] = {foo};
+
+extern void bar();
+
+int main()
+{
+  bar();
+  return 0;
+}