From e9302f35acfb3a2d7684addbccb6d0553c35faa9 Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Fri, 14 Oct 2022 16:41:48 -0400
Subject: [PATCH] Moved pragma rewrites to vf_rewrites.sh.

---
 .../preprocess_tasks_c.sh                     |  9 +----
 .../custom_build_scripts_RP2040/vf_rewrite.sh | 34 +++++++++++++++----
 2 files changed, 29 insertions(+), 14 deletions(-)

diff --git a/verification/verifast/custom_build_scripts_RP2040/preprocess_tasks_c.sh b/verification/verifast/custom_build_scripts_RP2040/preprocess_tasks_c.sh
index 1e840c7b0..9a3d0e857 100755
--- a/verification/verifast/custom_build_scripts_RP2040/preprocess_tasks_c.sh
+++ b/verification/verifast/custom_build_scripts_RP2040/preprocess_tasks_c.sh
@@ -8,7 +8,6 @@ DEMO_DIR="$PP_SCRIPT_WD/../FreeRTOS/Demo/CORTEX_M0+_RP2040/"
 TIMESTAMP=`date +'%y_%m_%d--%H_%M'`
 LOG_PP_OUT_DIR="$PP_SCRIPT_WD/log_preprocessed_files"
 LOG_PP_TASK_C="$LOG_PP_OUT_DIR/tasks--pp--$TIMESTAMP.c"
-LOG_PP_TASK_C_PRAGMA_COMMENTS="$LOG_PP_OUT_DIR/tasks--pp--pragma_comments--$TIMESTAMP.c"
 
 LOG_VF_RW_TASK_C="$LOG_PP_OUT_DIR/tasks--vf_rw--$TIMESTAMP.c"
 
@@ -30,15 +29,9 @@ echo "\n\nPreprocessed output with pragmas written to:"
 echo $LOG_PP_TASK_C
 
 
-sed 's|^#|// &|g' $LOG_PP_TASK_C  >  $LOG_PP_TASK_C_PRAGMA_COMMENTS
-
-echo "\n\nPreprocessed output with pragma comments written to:"
-echo $LOG_PP_TASK_C_PRAGMA_COMMENTS
-
-
 echo "\n\nApplying VeriFast rewrites. Result written to:"
 echo $LOG_VF_RW_TASK_C
-cp "$LOG_PP_TASK_C_PRAGMA_COMMENTS" "$LOG_VF_RW_TASK_C"
+cp "$LOG_PP_TASK_C" "$LOG_VF_RW_TASK_C"
 ./vf_rewrite.sh "$LOG_VF_RW_TASK_C"
 
 
diff --git a/verification/verifast/custom_build_scripts_RP2040/vf_rewrite.sh b/verification/verifast/custom_build_scripts_RP2040/vf_rewrite.sh
index 220ab4d9d..e325203a9 100755
--- a/verification/verifast/custom_build_scripts_RP2040/vf_rewrite.sh
+++ b/verification/verifast/custom_build_scripts_RP2040/vf_rewrite.sh
@@ -4,9 +4,31 @@ VF_RW_WD=`pwd`
 SOURCE_FILE="$1"
 BACKUP_IDX=0
 
-echo "VF RW: 'long unsigned int' -> 'unsinged long int'"
-echo "backup : $VF_RW_WD/$SOURCE_FILE.backup-$BACKUP_IDX"
-echo backup index $BACKUP_IDX
-sed -i."backup-$BACKUP_IDX" 's|long unsigned int|unsigned long int|g' $SOURCE_FILE
-((BACKUP_IDX=BACKUP_IDX+1))
-echo backup index $BACKUP_IDX
+
+# IMPORTANT:
+# None of the provided regexes must contain the unescaped character '|'
+#
+# $1 : sed 'find' regex
+# $2 : sed 'replace' regex
+rewrite()
+{
+  FIND_REGEX=$1
+  REPLACE_REGEX=$2
+  echo "VF RW: \"$FIND_REGEX\" -> \"$REPLACE_REGEX\""
+  echo "backup : $VF_RW_WD/$SOURCE_FILE.backup-$BACKUP_IDX"
+  sed -i."backup-$BACKUP_IDX" "s|$FIND_REGEX|$REPLACE_REGEX|g" $SOURCE_FILE
+  ((BACKUP_IDX=BACKUP_IDX+1))
+  echo "\n"
+}
+
+echo "Commenting out line/file pragmas"
+rewrite "^#" "// &"
+
+rewrite "long unsigned int" "unsigned long int"
+
+#echo "VF RW: 'long unsigned int' -> 'unsinged long int'"
+#echo "backup : $VF_RW_WD/$SOURCE_FILE.backup-$BACKUP_IDX"
+#echo backup index $BACKUP_IDX
+#sed -i."backup-$BACKUP_IDX" 's|long unsigned int|unsigned long int|g' $SOURCE_FILE
+#((BACKUP_IDX=BACKUP_IDX+1))
+#echo backup index $BACKUP_IDX