From 8b0048d48811968cfd8a63e06ddacd67c8fa512b Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Tue, 13 Dec 2022 10:05:22 -0500
Subject: [PATCH] Statup scripts ensure that output directories exist.

---
 .../VeriFast/tasks/vTaskSwitchContext/diff.sh | 11 +--------
 .../tasks/vTaskSwitchContext/paths.sh         | 23 +++++++++++++++++++
 .../tasks/vTaskSwitchContext/run-verifast.sh  |  1 +
 .../tasks/vTaskSwitchContext/run-vfide.sh     |  2 ++
 4 files changed, 27 insertions(+), 10 deletions(-)

diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/diff.sh b/Test/VeriFast/tasks/vTaskSwitchContext/diff.sh
index 3ce32909a..ac5c63c46 100755
--- a/Test/VeriFast/tasks/vTaskSwitchContext/diff.sh
+++ b/Test/VeriFast/tasks/vTaskSwitchContext/diff.sh
@@ -39,16 +39,7 @@ PP_VF_TASKS_C=`pp_vf_tasks_c $REPO_BASE_DIR`
 
 DIFF_REPORT=`diff_report $REPO_BASE_DIR`
 
-# Ensure that all output directories exist
-if [ ! -d "$LOG_DIR" ]; then
-    mkdir "$LOG_DIR"
-fi
-if [ ! -d "$STATS_DIR" ]; then
-    mkdir "$STATS_DIR"
-fi
-if [ ! -d "$PP_OUT_DIR" ]; then
-    mkdir "$PP_OUT_DIR"
-fi
+ensure_output_dirs_exist $REPO_BASE_DIR
 
 echo preprocessing production version of 'tasks.c'
 $PP $PROD_TASKS_C $PP_PROD_TASKS_C \
diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/paths.sh b/Test/VeriFast/tasks/vTaskSwitchContext/paths.sh
index 2ba420c46..42498376b 100755
--- a/Test/VeriFast/tasks/vTaskSwitchContext/paths.sh
+++ b/Test/VeriFast/tasks/vTaskSwitchContext/paths.sh
@@ -206,4 +206,27 @@ function diff_report() {
 }
 
 
+# Ensures that all potentially relevant output direcories exist.
+#
+# Expected arguments:
+# $1 : Absolute path to the repository's base 
+function ensure_output_dirs_exist() {
+    REPO_BASE_DIR="$1"
+
+    PP_OUT_DIR=`pp_out_dir $REPO_BASE_DIR`
+    STATS_DIR=`stats_dir $REPO_BASE_DIR`
+    PP_LOG_DIR=`pp_log_dir $REPO_BASE_DIR`
+    
+    if [ ! -d "$PP_OUT_DIR" ]; then
+        mkdir "$PP_OUT_DIR"
+    fi
+    if [ ! -d "$STATS_DIR" ]; then
+        mkdir "$STATS_DIR"
+    fi
+    if [ ! -d "$PP_LOG_DIR" ]; then
+        mkdir "$PP_LOG_DIR"
+    fi
+}
+
+
 
diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/run-verifast.sh b/Test/VeriFast/tasks/vTaskSwitchContext/run-verifast.sh
index 60d333daa..17fd35433 100755
--- a/Test/VeriFast/tasks/vTaskSwitchContext/run-verifast.sh
+++ b/Test/VeriFast/tasks/vTaskSwitchContext/run-verifast.sh
@@ -25,6 +25,7 @@ PROOF_FILES_DIR=`vf_proof_dir $REPO_BASE_DIR`
 PP_ERR_LOG="`pp_log_dir $REPO_BASE_DIR`/preprocessing_errors.txt"
 
 
+ensure_output_dirs_exist $REPO_BASE_DIR
 
 "$PREP" "$TASK_C" "$PP_TASK_C" "$PP_ERR_LOG" \
   "$REPO_BASE_DIR" "$VF_PROOF_BASE_DIR" "$VF_DIR"
diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/run-vfide.sh b/Test/VeriFast/tasks/vTaskSwitchContext/run-vfide.sh
index eb8b2b3ac..128fd9690 100755
--- a/Test/VeriFast/tasks/vTaskSwitchContext/run-vfide.sh
+++ b/Test/VeriFast/tasks/vTaskSwitchContext/run-vfide.sh
@@ -31,6 +31,8 @@ then
 fi
 
 
+ensure_output_dirs_exist $REPO_BASE_DIR
+
 "$PREP" "$TASK_C" "$PP_TASK_C" "$PP_ERR_LOG" \
   "$REPO_BASE_DIR" "$VF_PROOF_BASE_DIR" "$VF_DIR"