From d3cfeebca13baeb908d2728a978ab5d5198a3153 Mon Sep 17 00:00:00 2001 From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com> Date: Fri, 21 Oct 2022 17:42:05 -0400 Subject: [PATCH] Ensured that preprocessing script uses the smp demo submodule. --- .../custom_build_scripts_RP2040/preprocess_tasks_c.sh | 9 +++++---- 1 file changed, 5 insertions(+), 4 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 6dff52f2f..27e62385c 100755 --- a/verification/verifast/custom_build_scripts_RP2040/preprocess_tasks_c.sh +++ b/verification/verifast/custom_build_scripts_RP2040/preprocess_tasks_c.sh @@ -16,6 +16,7 @@ PP_OUT_DIR="$PP_SCRIPT_WD/../preprocessed_files" PP_TASK_C="$PP_OUT_DIR/tasks--pp.c" PICO_SDK_DIR="$PP_SCRIPT_WD/../sdks/pico-sdk" +SMP_DEMO_DIR="$PP_SCRIPT_WD/../demos/FreeRTOS-SMP-Demos" pwd mkdir $LOG_PP_OUT_DIR @@ -30,11 +31,11 @@ clang -E -C -DFREE_RTOS_KERNEL_SMP=1 -DLIB_FREERTOS_KERNEL=1 -DLIB_PICO_BIT_OPS -DVERIFAST \ -I/Users/reitobia/programs/verifast-21.04-83-gfae956f7/bin \ -I/Users/reitobia/repos2/FreeRTOS-Kernel/verification/verifast/proof_setup \ --I/Users/reitobia/repos2/FreeRTOS-Kernel/verification/verifast/demos/FreeRTOS-SMP-Demos/FreeRTOS/Demo/CORTEX_M0+_RP2040/OnEitherCore \ --I/Users/reitobia/repos2/FreeRTOS-Kernel/verification/verifast/demos/FreeRTOS-SMP-Demos/FreeRTOS/Source/portable/ThirdParty/GCC/RP2040/include \ --I/Users/reitobia/repos2/FreeRTOS-Kernel/verification/verifast/demos/FreeRTOS-SMP-Demos/FreeRTOS/Source/include \ +-I"$SMP_DEMO_DIR/FreeRTOS/Demo/CORTEX_M0+_RP2040/OnEitherCore" \ +-I"$SMP_DEMO_DIR/FreeRTOS/Source/portable/ThirdParty/GCC/RP2040/include" \ +-I"$SMP_DEMO_DIR/FreeRTOS/Source/include" \ -I"$PICO_SDK_DIR/src/common/pico_base/include" \ --I/Users/reitobia/repos2/FreeRTOS-Kernel/verification/verifast/demos/FreeRTOS-SMP-Demos/FreeRTOS/Demo/CORTEX_M0+_RP2040/build/generated/pico_base \ +-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" \