Merge pull request #5578 from tautschnig/goto-harness-windows

Make goto-harness-multi-file-project regression test work on Windows

Author: tautschnig

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

@@ -1,8 +1,12 @@
-if("${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
-  set(exclude_win_broken_tests -X winbug)
+if(WIN32)
+    set(is_windows true)
 else()
-  set(exclude_win_broken_tests "")
+    set(is_windows false)
 endif()
 
 add_test_pl_tests(
-  "${CMAKE_CURRENT_LIST_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-harness> $<TARGET_FILE:cbmc>" ${exclude_win_broken_tests})
+  "${CMAKE_CURRENT_LIST_DIR}/chain.sh \
+   $<TARGET_FILE:goto-cc> \
+   $<TARGET_FILE:goto-harness> \
+   $<TARGET_FILE:cbmc> \
+   ${is_windows}")

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

@@ -1,10 +1,25 @@
-default: test
+default: tests.log
+
+include ../../src/config.inc
+include ../../src/common
+
+GOTO_HARNESS_EXE=../../../src/goto-harness/goto-harness
+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 \
-		../../../src/goto-cc/goto-cc \
-	  ../../../src/goto-harness/goto-harness \
-		../../../src/cbmc/cbmc"
+	@../test.pl -e -p -c "../chain.sh $(GOTO_CC_EXE) $(GOTO_HARNESS_EXE) $(CBMC_EXE) $(is_windows)"
+
+tests.log: ../test.pl
+	@../test.pl -e -p -c "../chain.sh $(GOTO_CC_EXE) $(GOTO_HARNESS_EXE) $(CBMC_EXE) $(is_windows)"
+
 clean:
 	find -name '*.out' -execdir $(RM) '{}' \;
 	$(RM) tests.log

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

@@ -5,7 +5,8 @@ set -e
 goto_cc="$1"
 goto_harness="$2"
 cbmc="$3"
-goto_harness_args="${@:4:$#-4}"
+is_windows=$4
+goto_harness_args="${@:5:$#-5}"
 
 cleanup()
 {
@@ -14,19 +15,29 @@ cleanup()
 
 trap cleanup EXIT
 
-source_dir="$(pwd)"
-target_dir="$(mktemp -d)"
+# create the temporary directory relative to the current directory, thus
+# avoiding file names that start with a "/", which confuses goto-cl (Windows)
+# when running in git-bash.
+target_dir="$(TMPDIR=. mktemp -d)"
 
 # Compiling
-for file in "$source_dir"/*.c; do
+for file in *.c; do
   file_name="$(basename "$file")"
-  "$goto_cc" -c "$file" -o "$target_dir"/"${file_name%.c}.o"
+  if [[ "${is_windows}" == "true" ]]; then
+    "$goto_cc" "/c" "$file" "/Fo$target_dir/${file_name%.c}.obj"
+  else
+    "$goto_cc" -c "$file" -o "$target_dir"/"${file_name%.c}.o"
+  fi
 done
 
 # Linking
 
 main_exe="$target_dir/main.gb"
-"$goto_cc" "$target_dir"/*.o -o "$main_exe"
+if [[ "${is_windows}" == "true" ]]; then
+  "$goto_cc" "$target_dir"/*.obj "/Fe$main_exe"
+else
+  "$goto_cc" "$target_dir"/*.o -o "$main_exe"
+fi
 
 harness_out_file="$target_dir/harness.c"
 "$goto_harness" "$main_exe" "$harness_out_file" --harness-function-name harness $goto_harness_args

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

@@ -1,4 +1,4 @@
-CORE winbug
+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

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

@@ -1,4 +1,4 @@
-CORE winbug
+CORE
 dummy.c
 --function another --harness-type call-function
 ^EXIT=10$