simple test for mismatching return types accross compilation units

Author: Daniel Kroening

regression/cbmc/Linking7/return_type.desc

@@ -0,0 +1,10 @@
+KNOWNBUG
+return_type1.c
+return_type2.c
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Note issue #3081

regression/cbmc/Linking7/return_type1.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+
+struct S
+{
+  int i;
+};
+
+struct S *function();
+
+int main()
+{
+  assert(function() != 0);
+}

regression/cbmc/Linking7/return_type2.c

@@ -0,0 +1,10 @@
+struct S
+{
+  int i;
+  int j; // extra member
+} some_var;
+
+struct S *function()
+{
+  return &some_var;
+}