From 2ae20ff48d0962efabf5f0b1dcc451bec14c0dff Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Mon, 12 Dec 2022 08:26:42 -0500
Subject: [PATCH] Stored pp script args in diff script in variables to improve
 readability.

---
 .../VeriFast/tasks/vTaskSwitchContext/diff.sh | 34 +++++++++++--------
 1 file changed, 20 insertions(+), 14 deletions(-)

diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/diff.sh b/Test/VeriFast/tasks/vTaskSwitchContext/diff.sh
index 2afd3af95..292e04922 100755
--- a/Test/VeriFast/tasks/vTaskSwitchContext/diff.sh
+++ b/Test/VeriFast/tasks/vTaskSwitchContext/diff.sh
@@ -18,24 +18,30 @@ VF_PROOF_BASE_DIR=`vf_proof_base_dir $REPO_BASE_DIR`
 . "$PREFIX/paths.sh"
 
 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`
+
+# 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_PROD_TASKS_C=`pp_prod_tasks_c $REPO_BASE_DIR`
+PP_VF_TASKS_C=`pp_vf_tasks_c $REPO_BASE_DIR`
+
+echo PP_SCRIPT_DIR:
+echo $PP_SCRIPT_DIR
 
 echo preprocessing production version of 'tasks.c'
-"$PP_SCRIPT_DIR/preprocess_file_for_diff.sh" \
-    `prod_tasks_c $REPO_BASE_DIR` \
-    `pp_prod_tasks_c $REPO_BASE_DIR` \
-    "`pp_log_dir $REPO_BASE_DIR`/err1.txt" \
-    $REPO_BASE_DIR \
-    $VF_PROOF_BASE_DIR
+$PP $PROD_TASKS_C $PP_PROD_TASKS_C \
+    "$LOG_DIR/err1.txt" \
+    $REPO_BASE_DIR $VF_PROOF_BASE_DIR
 
 echo preprocessing verified version of 'tasks.c'
-"$PP_SCRIPT_DIR/preprocess_file_for_diff.sh" \
-    `vf_annotated_tasks_c $REPO_BASE_DIR` \
-    `pp_vf_tasks_c $REPO_BASE_DIR` \
-    "`pp_log_dir $REPO_BASE_DIR`/err2.txt" \
-    $REPO_BASE_DIR \
-    $VF_PROOF_BASE_DIR
+$PP $VF_TASKS_C $PP_VF_TASKS_C \
+    "$LOG_DIR/err2.txt" \
+    $REPO_BASE_DIR $VF_PROOF_BASE_DIR
 
 # pp script args
 # SRC_FILE="$1"
@@ -50,4 +56,4 @@ printf "\n\n\n"
 echo Diff:
 echo -----------------------------------------------------
 echo
-git diff --no-index "`pp_log_dir $REPO_BASE_DIR`/err1.txt" `pp_vf_tasks_c $REPO_BASE_DIR`
\ No newline at end of file
+git diff --no-index --ignore-all-space $PP_PROD_TASKS_C $PP_VF_TASKS_C
\ No newline at end of file