From dcbaf3863bd549573845c7f2d83487f4016ffc87 Mon Sep 17 00:00:00 2001 From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com> Date: Fri, 9 Dec 2022 10:35:20 -0500 Subject: [PATCH] Preprocessing script prefers modified files in proof subdirectory over files in main source and header dir. --- .../custom_build_scripts_RP2040/preprocess_tasks_c.sh | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) 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" \