Merge pull request diffblue#7225 from tautschnig/bugfixes/7156-contracts-linking

Linking: accept the same contract from multiple translation units

Author: tautschnig

regression/ansi-c/linking_contracts1/header.h

@@ -0,0 +1,20 @@
+#include <stdbool.h>
+
+bool util_func(int a)
+  // clang-format off
+  __CPROVER_ensures(
+    __CPROVER_return_value == true || __CPROVER_return_value == false)
+// clang-format on
+{
+  if(a > 0)
+  {
+    return true;
+  }
+  else
+  {
+    return false;
+  }
+}
+
+int test1(int a);
+int test2(int a);

regression/ansi-c/linking_contracts1/main.c

@@ -0,0 +1,6 @@
+#include "header.h"
+
+int test1(int a)
+{
+  return util_func(a);
+}

regression/ansi-c/linking_contracts1/module.c

@@ -0,0 +1,6 @@
+#include "header.h"
+
+int test2(int a)
+{
+  return util_func(a);
+}

regression/ansi-c/linking_contracts1/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+module.c
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
+conflict on code contract
+--
+This test makes sure we support contracts in header files, which may then end up
+in multiple translation units.

src/linking/linking.cpp

@@ -1105,10 +1105,15 @@ void linkingt::duplicate_non_type_symbol(
   symbolt &old_symbol,
   symbolt &new_symbol)
 {
-  // we do not permit multiple contracts to be defined, or cases where only one
-  // of the symbols is a contract
-  if(old_symbol.is_property || new_symbol.is_property)
+  // we do not permit different contracts with the same name to be defined, or
+  // cases where only one of the symbols is a contract
+  if(
+    old_symbol.is_property != new_symbol.is_property ||
+    (old_symbol.is_property && new_symbol.is_property &&
+     old_symbol.type != new_symbol.type))
+  {
     link_error(old_symbol, new_symbol, "conflict on code contract");
+  }
 
   // see if it is a function or a variable