Regression tests for same-named functions across translation units

regression/cbmc/Static_Functions1/resolve_a.c

@@ -0,0 +1,10 @@
+// file-local f, distinct from resolve_b.c's static f and the global f
+static int f(void)
+{
+  return 1;
+}
+
+int fa(void)
+{
+  return f();
+}

regression/cbmc/Static_Functions1/resolve_b.c

@@ -0,0 +1,10 @@
+// file-local f, distinct from resolve_a.c's static f and the global f
+static int f(void)
+{
+  return 2;
+}
+
+int fb(void)
+{
+  return f();
+}

regression/cbmc/Static_Functions1/resolve_main.c

@@ -0,0 +1,21 @@
+#include <assert.h>
+
+// Two further translation units (resolve_a.c, resolve_b.c) each define their
+// own file-local (static) function f, while this unit defines a global
+// (external linkage) f, all sharing the name f. Each call must resolve to the
+// definition mandated by the C standard: internal linkage stays within its
+// translation unit, external linkage is shared.
+int fa(void); // returns resolve_a.c's static f (== 1)
+int fb(void); // returns resolve_b.c's static f (== 2)
+
+int f(void) // the global f
+{
+  return 3;
+}
+
+int main(void)
+{
+  assert(fa() == 1);
+  assert(fb() == 2);
+  assert(f() == 3); // resolves to the global f defined above
+}

regression/cbmc/Static_Functions1/test-resolve.desc

@@ -0,0 +1,16 @@
+CORE
+resolve_main.c
+resolve_a.c resolve_b.c
+^\[main\.assertion\.1\] line 18 assertion fa\(\) == 1: SUCCESS$
+^\[main\.assertion\.2\] line 19 assertion fb\(\) == 2: SUCCESS$
+^\[main\.assertion\.3\] line 20 assertion f\(\) == 3: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Two translation units define a file-local (static) function named f, and a
+third defines a global f. Each call must resolve to the definition mandated
+by the C standard: the file-local calls stay within their unit, and the call
+from the unit defining the global f reaches that global.

regression/cbmc/Static_Functions1/test-unwind.desc

@@ -0,0 +1,20 @@
+CORE
+unwind_main.c
+unwind_a.c unwind_b.c --unwinding-assertions --unwindset 'count.0:4,count$link1.0:2'
+^\[count\.unwind\.0\] file unwind_b\.c line 6 unwinding assertion loop 0: FAILURE$
+^\[main\.assertion\.1\] line 13 assertion a_entry\(3\) == 3: SUCCESS$
+^\[main\.assertion\.2\] line 14 assertion b_entry\(3\) == 6: SUCCESS$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+file unwind_a\.c line 5 unwinding assertion loop 0: FAILURE
+--
+Two translation units define a file-local (static) function count, each with a
+loop. Linking renames the second, giving distinct loop identifiers count.0
+(unwind_a.c) and count$link1.0 (unwind_b.c). --unwindset uses those identifiers
+to bound the loops independently: count.0:4 is sufficient for unwind_a.c (no
+unwinding-assertion failure there), while count$link1.0:2 is too few for
+unwind_b.c and its unwinding assertion fails. This confirms the linker-renamed
+identifier selects the intended loop.

regression/cbmc/Static_Functions1/unwind_a.c

@@ -0,0 +1,13 @@
+// file-local count; its loop is identified as count.0 after linking
+static int count(int n)
+{
+  int s = 0;
+  for(int i = 0; i < n; i++)
+    s += 1;
+  return s;
+}
+
+int a_entry(int n)
+{
+  return count(n);
+}

regression/cbmc/Static_Functions1/unwind_b.c

@@ -0,0 +1,14 @@
+// file-local count with the same name as the one in unwind_a.c; after linking
+// its loop is renamed and identified as count$link1.0
+static int count(int n)
+{
+  int s = 0;
+  for(int i = 0; i < n; i++)
+    s += 2;
+  return s;
+}
+
+int b_entry(int n)
+{
+  return count(n);
+}

regression/cbmc/Static_Functions1/unwind_main.c

@@ -0,0 +1,15 @@
+#include <assert.h>
+
+// unwind_a.c and unwind_b.c both define a file-local (static) function named
+// count, each containing a loop. After linking, the second definition is
+// renamed, so the two loops carry distinct identifiers: count.0 (unwind_a.c)
+// and count$link1.0 (unwind_b.c). This shows those identifiers can be used
+// with --unwindset to bound each loop independently.
+int a_entry(int n);
+int b_entry(int n);
+
+int main(void)
+{
+  assert(a_entry(3) == 3);
+  assert(b_entry(3) == 6);
+}