Add test guarding for file local name mangler regression.

This is guarding for the regression described in github
issue #5380 and fixed in github PR #5402.

Author: NlightNFotis

regression/CMakeLists.txt

@@ -55,6 +55,7 @@ add_subdirectory(contracts)
 add_subdirectory(goto-harness)
 add_subdirectory(goto-harness-multi-file-project)
 add_subdirectory(goto-cc-file-local)
+add_subdirectory(goto-cc-regression-gh-issue-5380)
 add_subdirectory(linking-goto-binaries)
 add_subdirectory(symtab2gb)
 add_subdirectory(validate-trace-xml-schema)

regression/Makefile

@@ -28,6 +28,7 @@ DIRS = cbmc \
        systemc \
        contracts \
        goto-cc-file-local \
+       goto-cc-regression-gh-issue-5380 \
        linking-goto-binaries \
        symtab2gb \
        solver-hardness \

regression/goto-cc-regression-gh-issue-5380/CMakeLists.txt

@@ -0,0 +1,9 @@
+if(WIN32)
+    set(is_windows true)
+else()
+    set(is_windows false)
+endif()
+
+add_test_pl_tests(
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> ${is_windows}"
+)

regression/goto-cc-regression-gh-issue-5380/Makefile

@@ -0,0 +1,35 @@
+default: test.log
+
+include ../../src/config.inc
+include ../../src/common
+
+ifeq ($(BUILD_ENV_),MSVC)
+	exe=../../../src/goto-cc/goto-cl
+	is_windows=true
+else
+	exe=../../../src/goto-cc/goto-cc
+	is_windows=false
+endif
+
+test:
+	@../test.pl -e -p -c '../chain.sh $(exe) $(is_windows)'
+
+tests.log:
+	@../test.pl -e -p -c '../chain.sh $(exe) $(is_windows)'
+
+show:
+	@for dir in *; do
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	@for dir in *; do
+		$(RM) tests.log; \
+		if [ -d "$$dir" ]; then \
+			cd "$$dir"; \
+			$(RM) *.out *.gb; \
+			cd ..; \
+		fi; \
+	done;

regression/goto-cc-regression-gh-issue-5380/chain.sh

@@ -0,0 +1,33 @@
+#!/usr/bin/env bash
+#
+# This particular file and chain.sh make sure that a particular
+# file is passed twice to goto-cc, causing a crash under some
+# specific name mangling configuration.
+#
+# Author: Fotis Koutoulakis fotis.koutoulakis@diffblue.com
+
+set -e # cause the script to immediately exit when it errors
+
+goto_cc=$1
+is_windows=$2
+
+# collect compilation files
+PROBLEM_SRC="test.c"
+MAIN_SRC="main.c"
+
+echo "source files are ${SRC}"
+
+MAIN_OUTFILE="main.gb"
+PROBLEM_OUTFILE="test.gb"
+
+# first drive: compile the problematic file into a gb
+if [[ "${is_windows}" == "true" ]]; then
+  "${goto_cc}" --export-file-local-symbols "${PROBLEM_SRC}" /Fe"${PROBLEM_OUTFILE}"
+else
+  "${goto_cc}" --export-file-local-symbols "${PROBLEM_SRC}" -o "${PROBLEM_OUTFILE}"
+fi
+
+# second drive: compile and link the main source, problematic source and problematic
+# binary - note: the double inclusion of a similar artifact (source and binary) is
+# by design, to test a regression in goto-cc
+"${goto_cc}" --export-file-local-symbols "${PROBLEM_SRC}" "${MAIN_SRC}" "${PROBLEM_OUTFILE}"

regression/goto-cc-regression-gh-issue-5380/static-name-clash/main.c

@@ -0,0 +1,9 @@
+static inline int foo()
+{
+  return 42;
+}
+
+int bar()
+{
+  return foo();
+}

regression/goto-cc-regression-gh-issue-5380/static-name-clash/test.c

@@ -0,0 +1,11 @@
+static inline int foo()
+{
+  return 42;
+}
+
+int bar();
+
+int test()
+{
+  return foo() + bar();
+}

regression/goto-cc-regression-gh-issue-5380/static-name-clash/test.desc

@@ -0,0 +1,16 @@
+CORE
+test.c
+--export-function-local-symbols
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^Invariant check failed$
+--
+This test guards against a regression added when the local file
+name mangler would not add the required name into the symbol
+table. When the regression was present, we were met with an
+invariant violation during goto-cc compilation. Without it,
+nothing spectacular happens - compilation proceeds as expected.
+For more information look up issue 5380 in github.com/diffblue/cbmc.
+