Regression test scripts: use /Fe with goto-cl

Instead of a build-then-move dance, just use the appropriate
command-line flags. Some scripts already did this, now all of them do
so.

For goto-instrument/chain.sh that includes a more substantial cleanup
that removed a chunk of dead code ([[ x$name == x ]] was necessarily
false). Also, this script is no longer hard-coded to create main.gb as
output so as to permit multiple tests in the same directory (with
different target files) that could potentially be run concurrently.

Author: tautschnig

regression/contracts/chain.sh

@@ -21,8 +21,7 @@ else
 fi
 
 if [[ "${is_windows}" == "true" ]]; then
-  $goto_cc "${name}.c"
-  mv "${name}.exe" "${name}.gb"
+  $goto_cc "${name}.c" "/Fe${name}.gb"
 else
   $goto_cc -o "${name}.gb" "${name}.c"
 fi
@@ -35,8 +34,7 @@ elif echo $args_inst | grep -q -- "--dump-c" ; then
   mv "${name}-mod.gb" "${name}-mod.c"
 
   if [[ "${is_windows}" == "true" ]]; then
-    $goto_cc "${name}-mod.c"
-    mv "${name}-mod.exe" "${name}-mod.gb"
+    $goto_cc "${name}-mod.c" "/Fe${name}-mod.gb"
   else
     $goto_cc -o "${name}-mod.gb" "${name}-mod.c"
   fi

regression/goto-cc-cbmc-shared-options/chain.sh

@@ -12,8 +12,7 @@ base_name=${name%.c}
 base_name=${base_name%.cpp}
 
 if [[ "${is_windows}" == "true" ]]; then
-  "${goto_cc}" "${name}" ${options}
-  mv "${base_name}.exe" "${base_name}.gb"
+  "${goto_cc}" "${name}" ${options} "/Fe${base_name}.gb"
 else
   "${goto_cc}" "${name}" -o "${base_name}.gb" ${options}
 fi

regression/goto-cc-cbmc/chain.sh

@@ -12,8 +12,7 @@ base_name=${name%.c}
 base_name=${base_name%.cpp}
 
 if [[ "${is_windows}" == "true" ]]; then
-  "${goto_cc}" "${name}"
-  mv "${base_name}.exe" "${base_name}.gb"
+  "${goto_cc}" "${name}" "/Fe${base_name}.gb"
 else
   "${goto_cc}" "${name}" -o "${base_name}.gb"
 fi

regression/goto-cc-goto-analyzer/chain.sh

@@ -15,8 +15,7 @@ if test -f ${buildgoto}; then
   ./${buildgoto} ${goto_cc} ${is_windows}
 else
   if [[ "${is_windows}" == "true" ]]; then
-    "${goto_cc}" "${name}.c"
-    mv "${name}.exe" "${name}.gb"
+    "${goto_cc}" "${name}.c" "/Fe${name}.gb"
   else
     "${goto_cc}" "${name}.c" -o "${name}.gb"
   fi

regression/goto-cc-multi-file/chain.sh

@@ -11,8 +11,7 @@ name=${*:$#}
 name=${name%.c}
 
 if [[ "${is_windows}" == "true" ]]; then
-  ${goto_cc} ${name}.c ${args}
-  mv ${name}.exe ${name}.gb
+  ${goto_cc} ${name}.c ${args} "/Fe${name}.gb"
 else
   ${goto_cc} ${name}.c ${args} -o ${name}.gb
 fi

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

@@ -22,7 +22,7 @@ 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}"
+  "${goto_cc}" --export-file-local-symbols "${PROBLEM_SRC}" "/Fe${PROBLEM_OUTFILE}"
 else
   "${goto_cc}" --export-file-local-symbols "${PROBLEM_SRC}" -o "${PROBLEM_OUTFILE}"
 fi

regression/goto-harness/chain.sh

@@ -26,8 +26,7 @@ args=${*:1:$#-1}
 
 
 if [[ "${is_windows}" == "true" ]]; then
-  $goto_cc "$input_c_file"
-  mv "${name}.exe" "$input_goto_binary"
+  $goto_cc "$input_c_file" "/Fe$input_goto_binary"
 else
   $goto_cc -o "$input_goto_binary" "$input_c_file"
 fi

regression/goto-instrument-typedef/chain.sh

@@ -13,8 +13,7 @@ args=${*:4:$#-4}
 
 rm -f "${name}.gb"
 if [[ "${is_windows}" == "true" ]]; then
-  "$GC" "${name}.c" --function fun
-  mv "${name}.exe" "${name}.gb"
+  "$GC" "${name}.c" --function fun "/Fe${name}.gb"
 else
   "$GC" "${name}.c" --function fun -o "${name}.gb"
 fi

regression/goto-instrument/chain.sh

@@ -7,48 +7,37 @@ goto_instrument=$2
 cbmc=$3
 is_windows=$4
 
-name=${*:$#}
-
-if [[ x$name == x ]];  then
-  name=${name%.c}
-fi
-
+sources=${*:$#}
 args=${*:5:$#-5}
 
-if [[ "${is_windows}" == "true" && x$name != x ]]; then
-  $goto_cc "main.gb" ${name}
-  name="main"
-  mv "${name}.exe" "${name}.gb"
-elif [[ "${is_windows}" == "true" ]]; then
-  $goto_cc "${name}.c"
-  mv "${name}.exe" "${name}.gb"
-elif [[ x$name != x ]]; then
-  $goto_cc -o "main.gb" ${name}
-  echo "name: ${name}"
-  name="main"
+set -- $sources
+target=${*:$#}
+target=${target%.c}
+
+if [[ "${is_windows}" == "true" ]]; then
+  $goto_cc ${sources} "/Fe${target}.gb"
 else
-  $goto_cc -o "${name}.gb" "${name}.c"
+  $goto_cc -o ${target}.gb ${sources}
 fi
 
-rm -f "${name}-mod.gb"
-$goto_instrument ${args} "${name}.gb" "${name}-mod.gb"
-if [ ! -e "${name}-mod.gb" ] ; then
-  cp "$name.gb" "${name}-mod.gb"
+rm -f "${target}-mod.gb"
+$goto_instrument ${args} "${target}.gb" "${target}-mod.gb"
+if [ ! -e "${target}-mod.gb" ] ; then
+  cp "${target}.gb" "${target}-mod.gb"
 elif echo $args | grep -q -- "--dump-c-type-header" ; then
-  cat "${name}-mod.gb"
-  mv "${name}.gb" "${name}-mod.gb"
+  cat "${target}-mod.gb"
+  mv "${target}.gb" "${target}-mod.gb"
 elif echo $args | grep -q -- "--dump-c" ; then
-  cat "${name}-mod.gb"
-  mv "${name}-mod.gb" "${name}-mod.c"
+  cat "${target}-mod.gb"
+  mv "${target}-mod.gb" "${target}-mod.c"
 
   if [[ "${is_windows}" == "true" ]]; then
-    $goto_cc "${name}-mod.c"
-    mv "${name}-mod.exe" "${name}-mod.gb"
+    $goto_cc "${target}-mod.c" "/Fe${target}-mod.gb"
   else
-    $goto_cc -o "${name}-mod.gb" "${name}-mod.c"
+    $goto_cc -o "${target}-mod.gb" "${target}-mod.c"
   fi
 
-  rm "${name}-mod.c"
+  rm "${target}-mod.c"
 fi
-$goto_instrument --show-goto-functions "${name}-mod.gb"
-$cbmc "${name}-mod.gb"
+$goto_instrument --show-goto-functions "${target}-mod.gb"
+$cbmc "${target}-mod.gb"

regression/goto-interpreter/chain.sh

@@ -11,8 +11,7 @@ name=${*:$#}
 base_name=${name%.c}
 
 if [[ "${is_windows}" == "true" ]]; then
-  "${goto_cc}" "${name}"
-  mv "${base_name}.exe" "${base_name}.gb"
+  "${goto_cc}" "${name}" "/Fe${base_name}.gb"
 else
   "${goto_cc}" "${name}" -o "${base_name}.gb"
 fi