Add regression test to check that linking succeeds

Simple test of calling a function defined in a separate binary. First compile
both with goto-cc and then call cbmc on the two binaries.

Author: petr-bauch

regression/CMakeLists.txt

@@ -51,3 +51,4 @@ add_subdirectory(systemc)
 add_subdirectory(contracts)
 add_subdirectory(goto-harness)
 add_subdirectory(goto-cc-file-local)
+add_subdirectory(linking-goto-binaries)

regression/Makefile

@@ -26,6 +26,7 @@ DIRS = cbmc \
        systemc \
        contracts \
        goto-cc-file-local \
+       linking-goto-binaries \
        # Empty last line
 
 # Run all test directories in sequence

regression/linking-goto-binaries/CMakeLists.txt

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

regression/linking-goto-binaries/Makefile

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

regression/linking-goto-binaries/chain.sh

@@ -0,0 +1,25 @@
+#!/bin/bash
+
+set -e
+
+goto_cc=$1
+cbmc=$2
+is_windows=$3
+entry_point='generated_entry_function'
+
+main=${*:$#}
+main=${main%.c}
+args=${*:4:$#-4}
+next=${args%.c}
+
+if [[ "${is_windows}" == "true" ]]; then
+  $goto_cc "${main}.c"
+  $goto_cc "${next}.c"
+  mv "${main}.exe" "${main}.gb"
+  mv "${next}.exe" "${next}.gb"
+else
+  $goto_cc -o "${main}.gb" "${main}.c"
+  $goto_cc -o "${next}.gb" "${next}.c"
+fi
+
+$cbmc "${main}.gb" "${next}.gb"

regression/linking-goto-binaries/simple_function_call/main.c

@@ -0,0 +1,11 @@
+#include "supp.h"
+#include <assert.h>
+
+const int five = 5;
+
+int main()
+{
+  int ten = times_two(five);
+  assert(ten == 10);
+  return 0;
+}

regression/linking-goto-binaries/simple_function_call/supp.c

@@ -0,0 +1,6 @@
+#include "supp.h"
+
+int times_two(int i)
+{
+  return 2 * i;
+}

regression/linking-goto-binaries/simple_function_call/supp.h

@@ -0,0 +1,6 @@
+#ifndef SUPP_H
+#define SUPP_H
+
+int times_two(int i);
+
+#endif // SUPP_H

regression/linking-goto-binaries/simple_function_call/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+supp.c
+^EXIT=0$
+^SIGNAL=0$
+\[main.assertion.1\] line [0-9]+ assertion ten == 10: SUCCESS
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring