Add regression test to check for changes in goto-harness filtering

Author: hannes-steffenhagen-diffblue

regression/CMakeLists.txt

@@ -52,6 +52,7 @@ add_subdirectory(statement-list)
 add_subdirectory(systemc)
 add_subdirectory(contracts)
 add_subdirectory(goto-harness)
+add_subdirectory(goto-harness-multi-file-project)
 add_subdirectory(goto-cc-file-local)
 add_subdirectory(linking-goto-binaries)
 add_subdirectory(symtab2gb)

regression/goto-harness-multi-file-project/CMakeLists.txt

@@ -0,0 +1,2 @@
+add_test_pl_tests(
+  "${CMAKE_CURRENT_LIST_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-harness> $<TARGET_FILE:cbmc>")

regression/goto-harness-multi-file-project/Makefile

@@ -0,0 +1,10 @@
+default: test
+
+test:
+	@../test.pl -e -p -c "../chain.sh \
+		../../../src/goto-cc/goto-cc \
+	  ../../../src/goto-harness/goto-harness \
+		../../../src/cbmc/cbmc"
+clean:
+	find -name '*.out' -execdir $(RM) '{}' \;
+	$(RM) tests.log

regression/goto-harness-multi-file-project/chain.sh

@@ -0,0 +1,28 @@
+#!/bin/bash
+
+set -x
+set -e
+goto_cc="$1"
+goto_harness="$2"
+cbmc="$3"
+goto_harness_args="${@:4:$#-4}"
+
+source_dir="$(pwd)"
+target_dir="$(mktemp -d)"
+
+# Compiling
+for file in "$source_dir"/*.c; do
+  file_name="$(basename "$file")"
+  "$goto_cc" -c "$file" -o "$target_dir"/"${file_name%.c}.o"
+done
+
+# Linking
+
+main_exe="$target_dir/main.gb"
+"$goto_cc" "$target_dir"/*.o -o "$main_exe"
+
+harness_out_file="$target_dir/harness.c"
+"$goto_harness" "$main_exe" "$harness_out_file" --harness-function-name harness $goto_harness_args
+cat "$harness_out_file"
+"$cbmc" "$main_exe" "$harness_out_file" --function harness
+

regression/goto-harness-multi-file-project/static_functions/main.c

@@ -0,0 +1,10 @@
+#include "service.h"
+
+// this isn't testing any interesting harness
+// properties so we just have a main function
+// with no parameters
+int main(void)
+{
+  service_t *service = get_default_service();
+  service_serve(service);
+}

regression/goto-harness-multi-file-project/static_functions/service.c

@@ -0,0 +1,31 @@
+#include "service.h"
+#include <assert.h>
+
+// contents of the struct
+// (mostly just a vtable)
+
+struct service
+{
+  void (*serve)(void);
+};
+
+void service_serve(service_t *service)
+{
+  service->serve();
+}
+
+static void default_serve(void)
+{
+  assert(0 && "default serve should fail so we can see it is being called");
+}
+
+// this static initialisation should not show up in output
+// in fact, there is a bit of a bug with dump-c where this
+// initialisation would appear but the default_serve function
+// would be omitted in certain cases.
+static service_t default_service = {.serve = default_serve};
+
+service_t *get_default_service(void)
+{
+  return &default_service;
+}

regression/goto-harness-multi-file-project/static_functions/service.h

@@ -0,0 +1,13 @@
+#include <stddef.h>
+
+// common pattern:
+// Some sort of interface defined over "abstract" type with hidden
+// implementation details, effectively C style OOP
+//
+// This is a straw example of course, but very reminiscent of patterns that
+// occur in real programs
+
+typedef struct service service_t;
+
+service_t *get_default_service(void);
+void service_serve(service_t *service);

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

@@ -0,0 +1,12 @@
+CORE
+dummy.c
+--function main --harness-type call-function
+\[default_serve\.assertion\.1\] line \d+ assertion 0 && \"default serve should fail so we can see it is being called\": FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+static void default_serve
+--
+When running the harness we should run into the assertion failure from the
+static default_serve function, but the harness C code should not contain this
+or any other static functions or variables.