Add test for fixing of referencing of static symbols in harness file.

Author: NlightNFotis

regression/goto-harness-multi-file-project/static_symbols_referencing/first_one.c

@@ -0,0 +1,25 @@
+#include "first_one.h"
+#include <assert.h>
+
+static int static_function(int a)
+{
+  assert(a == 0);
+  return a;
+}
+
+int non_static_function(int a)
+{
+  return static_function(a);
+}
+
+static int with_matching_signature(int a)
+{
+  assert(0 && "this is not reachable as far as goto-harness is concerned");
+  return 0;
+}
+
+void non_static_with_non_matching_signature(void)
+{
+  // this is just here so `static_with_matching_signature` has a non-file-local use
+  assert(static_with_matching_signature(10) == 10);
+}

regression/goto-harness-multi-file-project/static_symbols_referencing/first_one.h

@@ -0,0 +1 @@
+int non_static_function(int a);

regression/goto-harness-multi-file-project/static_symbols_referencing/second_one.c

@@ -0,0 +1,8 @@
+#include "first_one.h"
+
+int another(int (*fun_ptr)(int), int c)
+{
+  int a = (*fun_ptr)(c);
+
+  return a;
+}

regression/goto-harness-multi-file-project/static_symbols_referencing/test.desc

@@ -0,0 +1,15 @@
+CORE
+dummy.c
+--function another --harness-type call-function
+^EXIT=10$
+^SIGNAL=0$
+\[static_function\.assertion\.1\] line \d assertion a == 0: FAILURE
+\[non_static_with_non_matching_signature\.assertion\.1] line \d+ assertion static_with_matching_signature\(10\) == 10: SUCCESS
+
+^VERIFICATION FAILED$
+--
+^CONVERSION ERROR$
+--
+For this particular error, we care mostly that goto-harness
+doesn't reference static symbols in other files, which would
+cause analysis through CBMC to fail with a conversion error.