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

Author: NlightNFotis

regression/CMakeLists.txt

@@ -53,6 +53,7 @@ add_subdirectory(statement-list)
 add_subdirectory(systemc)
 add_subdirectory(contracts)
 add_subdirectory(goto-harness)
+add_subdirectory(goto-harness-gb-input)
 add_subdirectory(goto-harness-multi-file-project)
 add_subdirectory(goto-cc-file-local)
 add_subdirectory(goto-cc-regression-gh-issue-5380)

regression/Makefile

@@ -20,6 +20,7 @@ DIRS = cbmc \
        goto-analyzer-taint \
        goto-gcc \
        goto-harness \
+       goto-harness-gb-input \
        goto-cl \
        goto-cc-cbmc \
        cbmc-cpp \

regression/goto-harness-gb-input/CMakeLists.txt

@@ -0,0 +1,4 @@
+add_test_pl_tests(
+  "../chain.sh \
+  $<TARGET_FILE:goto-harness> \
+  $<TARGET_FILE:cbmc>")

regression/goto-harness-gb-input/Makefile

@@ -0,0 +1,18 @@
+default: tests.log
+
+include ../../src/config.inc
+include ../../src/common
+
+GOTO_HARNESS_EXE=../../../src/goto-harness/goto-harness
+CBMC_EXE=../../../src/cbmc/cbmc
+
+test:
+	@../test.pl -e -p -c "../chain.sh $(GOTO_HARNESS_EXE) $(CBMC_EXE)"
+
+tests.log: ../test.pl
+	@../test.pl -e -p -c "../chain.sh $(GOTO_HARNESS_EXE) $(CBMC_EXE)"
+
+clean:
+	find -name '*.out' -execdir $(RM) '{}' \;
+	find -name '*.gb' -execdir $(RM) {} \;
+	$(RM) tests.log

regression/goto-harness-gb-input/chain.sh

@@ -0,0 +1,18 @@
+#!/bin/bash
+
+set -e
+
+goto_harness=$1
+cbmc=$2
+
+input_goto_binary=${*:$#}
+args=${*:3:$#-3}
+harness_c_file="generated-harness-file.c"
+entry_point='generated_harness_test_function'
+
+if [ -e "$harness_c_file" ]; then
+  rm -rf "$harness_c_file"
+fi
+
+$goto_harness "$input_goto_binary" "$harness_c_file" ${args}
+$cbmc "$harness_c_file"

regression/goto-harness-gb-input/static-symbol-referencing/aws_byte_buf_append_harness.goto

@@ -0,0 +1,11 @@
+CORE
+aws_byte_buf_append_harness.goto
+--harness-type call-function --harness-function-name generated_harness_test_function --function aws_byte_buf_append
+^EXIT=6$
+^SIGNAL=0$
+--
+^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