From c50e8bd5b335ab44828db2c2043bd1c3c604cc15 Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Mon, 12 Dec 2022 10:01:53 -0500
Subject: [PATCH] Diff report is now written to file.

---
 .../preprocess_file_for_diff.sh               |  2 --
 .../VeriFast/tasks/vTaskSwitchContext/diff.sh | 25 ++++++++++++++-----
 .../tasks/vTaskSwitchContext/paths.sh         | 24 ++++++++++++++++++
 .../vTaskSwitchContext/stats/diff_report.txt  |  0
 4 files changed, 43 insertions(+), 8 deletions(-)
 create mode 100644 Test/VeriFast/tasks/vTaskSwitchContext/stats/diff_report.txt

diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/custom_build_scripts_RP2040/preprocess_file_for_diff.sh b/Test/VeriFast/tasks/vTaskSwitchContext/custom_build_scripts_RP2040/preprocess_file_for_diff.sh
index 62cd49a14..a432bc1e3 100755
--- a/Test/VeriFast/tasks/vTaskSwitchContext/custom_build_scripts_RP2040/preprocess_file_for_diff.sh
+++ b/Test/VeriFast/tasks/vTaskSwitchContext/custom_build_scripts_RP2040/preprocess_file_for_diff.sh
@@ -24,8 +24,6 @@ echo $VF_PROOF_BASE_DIR
 . "`pp_script_dir $REPO_BASE_DIR`/pp_flags.sh" "$REPO_BASE_DIR" "$VF_PROOF_BASE_DIR"
 
 PROD_HEADER_DIR=`prod_header_dir $REPO_BASE_DIR`
-ls PROD_HEADER_DIR
-ls $PROD_HEADER_DIR
 
 
 # Relevant clang flags:
diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/diff.sh b/Test/VeriFast/tasks/vTaskSwitchContext/diff.sh
index 33928cf08..85f0c0833 100755
--- a/Test/VeriFast/tasks/vTaskSwitchContext/diff.sh
+++ b/Test/VeriFast/tasks/vTaskSwitchContext/diff.sh
@@ -21,16 +21,29 @@ VF_PROOF_DIR=`vf_proof_base_dir $REPO_BASE_DIR`
 PP_SCRIPT_DIR=`pp_script_dir $REPO_BASE_DIR`
 PP="$PP_SCRIPT_DIR/preprocess_file_for_diff.sh"
 LOG_DIR=`pp_log_dir $REPO_BASE_DIR`
+STATS_DIR=`stats_dir $REPO_BASE_DIR`
 
 # Unpreprocessed verions of tasks.c
 PROD_TASKS_C=`prod_tasks_c $REPO_BASE_DIR`
 VF_TASKS_C=`vf_annotated_tasks_c $REPO_BASE_DIR`
 
 # Preprocessed versions of tasks.c
+PP_OUT_DIR=`pp_out_dir $REPO_BASE_DIR`
 PP_PROD_TASKS_C=`pp_prod_tasks_c $REPO_BASE_DIR`
 PP_VF_TASKS_C=`pp_vf_tasks_c $REPO_BASE_DIR`
 
-mkdir "$LOG_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
 
 echo preprocessing production version of 'tasks.c'
 $PP $PROD_TASKS_C $PP_PROD_TASKS_C \
@@ -51,8 +64,8 @@ $PP $VF_TASKS_C $PP_VF_TASKS_C \
 
 
 
-printf "\n\n\n"
-echo Diff:
-echo -----------------------------------------------------
-echo
-git diff --no-index --ignore-all-space $PP_PROD_TASKS_C $PP_VF_TASKS_C
\ No newline at end of file
+echo Computing diff. Output written to:
+echo \"$DIFF_REPORT\"
+
+git diff --no-index --ignore-all-space $PP_PROD_TASKS_C $PP_VF_TASKS_C \
+> "$DIFF_REPORT"
\ No newline at end of file
diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/paths.sh b/Test/VeriFast/tasks/vTaskSwitchContext/paths.sh
index 21cd42f14..2ba420c46 100755
--- a/Test/VeriFast/tasks/vTaskSwitchContext/paths.sh
+++ b/Test/VeriFast/tasks/vTaskSwitchContext/paths.sh
@@ -183,3 +183,27 @@ function smp_demo_dir() {
 }
 
 
+# Returns the absolute path to directory where the statistic reports are stored.
+#
+# Expected arguments:
+# $1 : Absolute path to the repository's base 
+function stats_dir() {
+    REPO_BASE_DIR="$1"
+    VF_PROOF_DIR=`vf_proof_base_dir $REPO_BASE_DIR`
+
+    echo "$VF_PROOF_DIR/stats"
+}
+
+# Returns the absolute path to diff report.
+#
+# Expected arguments:
+# $1 : Absolute path to the repository's base 
+function diff_report() {
+    REPO_BASE_DIR="$1"
+    STATS_DIR=`stats_dir $REPO_BASE_DIR`
+
+    echo "$STATS_DIR/diff_report.txt"
+}
+
+
+
diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/stats/diff_report.txt b/Test/VeriFast/tasks/vTaskSwitchContext/stats/diff_report.txt
new file mode 100644
index 000000000..e69de29bb