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 e2a9fefbc..83102aec6 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 @@ -9,9 +9,10 @@ VF_DIR="$1" 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" - -TASKS_C="$REPO_BASE_DIR/tasks.c" +TASKS_C="$VF_PROOF_MOD_SRC_DIR/tasks.c" PROOF_SETUP_DIR="$VF_PROOF_BASE_DIR/proof_setup" PROOF_FILES_DIR="$VF_PROOF_BASE_DIR/proof" @@ -49,6 +50,8 @@ clang -E -C -DFREE_RTOS_KERNEL_SMP=1 -DLIB_FREERTOS_KERNEL=1 -DLIB_PICO_BIT_OPS -DVERIFAST \ -DVERIFAST_SKIP_BITVECTOR_PROOF__STACK_ALIGNMENT \ -I"$VF_DIR/bin" \ +-I"$VF_PROOF_MOD_HEADER_DIR" \ +-I"$VF_PROOF_MOD_SRC_DIR" \ -I"$PROOF_SETUP_DIR" \ -I"$PROOF_FILES_DIR" \ -I"$SMP_DEMO_DIR/FreeRTOS/Demo/CORTEX_M0+_RP2040/OnEitherCore" \