From 21992b6c34bbbd2059ca9013fcc71598535b5149 Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Fri, 9 Dec 2022 14:51:00 -0500
Subject: [PATCH] Startup script expects paths to relevant directories as
 arguments instead of computing them itself.

---
 .../preprocess_file.sh                           |  0
 .../preprocess_tasks_c.sh                        | 16 +++++++++++-----
 .../start-vfide--preprocessed.sh                 | 10 ++++++----
 3 files changed, 17 insertions(+), 9 deletions(-)
 create mode 100755 Test/VeriFast/tasks/vTaskSwitchContext/custom_build_scripts_RP2040/preprocess_file.sh

diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/custom_build_scripts_RP2040/preprocess_file.sh b/Test/VeriFast/tasks/vTaskSwitchContext/custom_build_scripts_RP2040/preprocess_file.sh
new file mode 100755
index 000000000..e69de29bb
diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/custom_build_scripts_RP2040/preprocess_tasks_c.sh b/Test/VeriFast/tasks/vTaskSwitchContext/custom_build_scripts_RP2040/preprocess_tasks_c.sh
index 83102aec6..5dc1720ae 100755
--- a/Test/VeriFast/tasks/vTaskSwitchContext/custom_build_scripts_RP2040/preprocess_tasks_c.sh
+++ b/Test/VeriFast/tasks/vTaskSwitchContext/custom_build_scripts_RP2040/preprocess_tasks_c.sh
@@ -2,13 +2,15 @@
 ps -o comm= -p $$
 
 # This script expects the following command line arguments:
-# $1 : Absolute path to the VeriFast directory
+# $1 : Absolute path to the root dir of this repository
+# $2 : Absolute path to the root of the directory containing the VeriFast proofs
+# $3 : Absolute path to the VeriFast directory
 
-VF_DIR="$1"
+REPO_BASE_DIR="$1"
+VF_PROOF_BASE_DIR="$2"
+VF_DIR="$3"
 
 PP_SCRIPT_WD=`pwd`
-REPO_BASE_DIR=`cd ../../../../..; pwd`
-VF_PROOF_BASE_DIR=`cd ..; pwd`
 VF_PROOF_MOD_SRC_DIR="$VF_PROOF_BASE_DIR/src"
 VF_PROOF_MOD_HEADER_DIR="$VF_PROOF_BASE_DIR/include"
 
@@ -47,6 +49,7 @@ mkdir $LOG_PP_OUT_DIR
 
 echo start preprocessor
 clang -E -C  -DFREE_RTOS_KERNEL_SMP=1 -DLIB_FREERTOS_KERNEL=1 -DLIB_PICO_BIT_OPS=1 -DLIB_PICO_BIT_OPS_PICO=1 -DLIB_PICO_DIVIDER=1 -DLIB_PICO_DIVIDER_HARDWARE=1 -DLIB_PICO_DOUBLE=1 -DLIB_PICO_DOUBLE_PICO=1 -DLIB_PICO_FLOAT=1 -DLIB_PICO_FLOAT_PICO=1 -DLIB_PICO_INT64_OPS=1 -DLIB_PICO_INT64_OPS_PICO=1 -DLIB_PICO_MALLOC=1 -DLIB_PICO_MEM_OPS=1 -DLIB_PICO_MEM_OPS_PICO=1 -DLIB_PICO_MULTICORE=1 -DLIB_PICO_PLATFORM=1 -DLIB_PICO_PRINTF=1 -DLIB_PICO_PRINTF_PICO=1 -DLIB_PICO_RUNTIME=1 -DLIB_PICO_STANDARD_LINK=1 -DLIB_PICO_STDIO=1 -DLIB_PICO_STDIO_UART=1 -DLIB_PICO_STDLIB=1 -DLIB_PICO_SYNC=1 -DLIB_PICO_SYNC_CORE=1 -DLIB_PICO_SYNC_CRITICAL_SECTION=1 -DLIB_PICO_SYNC_MUTEX=1 -DLIB_PICO_SYNC_SEM=1 -DLIB_PICO_TIME=1 -DLIB_PICO_UTIL=1 -DPICO_BOARD=\"pico\" -DPICO_BUILD=1 -DPICO_CMAKE_BUILD_TYPE=\"Release\" -DPICO_COPY_TO_RAM=0 -DPICO_CXX_ENABLE_EXCEPTIONS=0 -DPICO_NO_FLASH=0 -DPICO_NO_HARDWARE=0 -DPICO_ON_DEVICE=1 -DPICO_STACK_SIZE=0x1000 -DPICO_TARGET_NAME=\"on_core_one\" -DPICO_USE_BLOCKED_RAM=0 -DmainRUN_FREE_RTOS_ON_CORE=1 \
+\
 -DVERIFAST \
 -DVERIFAST_SKIP_BITVECTOR_PROOF__STACK_ALIGNMENT \
 -I"$VF_DIR/bin" \
@@ -54,12 +57,15 @@ clang -E -C  -DFREE_RTOS_KERNEL_SMP=1 -DLIB_FREERTOS_KERNEL=1 -DLIB_PICO_BIT_OPS
 -I"$VF_PROOF_MOD_SRC_DIR" \
 -I"$PROOF_SETUP_DIR" \
 -I"$PROOF_FILES_DIR" \
+\
 -I"$SMP_DEMO_DIR/FreeRTOS/Demo/CORTEX_M0+_RP2040/OnEitherCore" \
+-I"$SMP_DEMO_DIR/FreeRTOS/Demo/CORTEX_M0+_RP2040/build/generated/pico_base" \
+\
 -I"$REPO_BASE_DIR/portable/ThirdParty/GCC/RP2040/include" \
 -I"$REPO_BASE_DIR/portable/ThirdParty/GCC/RP2040" \
 -I"$REPO_BASE_DIR/include" \
+\
 -I"$PICO_SDK_DIR/src/common/pico_base/include" \
--I"$SMP_DEMO_DIR/FreeRTOS/Demo/CORTEX_M0+_RP2040/build/generated/pico_base" \
 -I"$PICO_SDK_DIR/src/boards/include" \
 -I"$PICO_SDK_DIR/src/rp2_common/pico_platform/include" \
 -I"$PICO_SDK_DIR/src/rp2040/hardware_regs/include" \
diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/start-vfide--preprocessed.sh b/Test/VeriFast/tasks/vTaskSwitchContext/start-vfide--preprocessed.sh
index b288dc70a..6f506fc8f 100755
--- a/Test/VeriFast/tasks/vTaskSwitchContext/start-vfide--preprocessed.sh
+++ b/Test/VeriFast/tasks/vTaskSwitchContext/start-vfide--preprocessed.sh
@@ -5,7 +5,9 @@
 # $1 : Absolute path to the VeriFast directory
 
 
-VF_DIR="$1"
+REPO_BASE_DIR="$1"
+VF_PROOF_BASE_DIR="$2"
+VF_DIR="$3"
 echo Path to vfide binary : "\'$VFIDE\'"
 
 START_WD=`pwd`
@@ -14,9 +16,9 @@ PP_SCRIPT="./preprocess_tasks_c.sh"
 PP_TASK_C="$START_WD/preprocessed_files/tasks__pp.c"
 
 FONT_SIZE=17
-if [ "$2" != "" ]
+if [ "$4" != "" ]
 then
-  FONT_SIZE="$2"
+  FONT_SIZE="$4"
 fi
 
 # Flags to SKIP expensive proofs:
@@ -27,7 +29,7 @@ fi
 cd "$PP_SCRIPT_DIR"
 pwd
 ls
-"$PP_SCRIPT" "$VF_DIR"
+"$PP_SCRIPT" "$REPO_BASE_DIR" "$VF_PROOF_BASE_DIR" "$VF_DIR"
 cd "$START_WD"
 
 echo "\n\nPreprocessing script finished\n\n"