len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-12-11 22:25:14 -05:00
Code Issues Projects Releases Packages Wiki Activity

Preprocessing script prefers modified files in proof subdirectory over files in main source and header dir.

Browse source
This commit is contained in:
Tobias Reinhard 2022-12-09 10:35:20 -05:00
parent cc7ed1e3eb
commit dcbaf3863b
1 changed files with 5 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

7
Test/VeriFast/tasks/vTaskSwitchContext/custom_build_scripts_RP2040/preprocess_tasks_c.sh
View file

@ -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" \