From 21f9a95a1090b8f054da405db98d695ece0db3f6 Mon Sep 17 00:00:00 2001 From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com> Date: Thu, 13 Oct 2022 09:48:11 -0400 Subject: [PATCH] Fixed proof setup include path The include path contained some directories within the SMP demos FreeRTOS source tree (which is the official unaltered FreeRTOS repo). Updated the include path such that it points to our forked version of the FreeRTOS kernel repo. --- verification/verifast/start-vfide.sh | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/verification/verifast/start-vfide.sh b/verification/verifast/start-vfide.sh index a49fcd657..5e5c9bc2a 100755 --- a/verification/verifast/start-vfide.sh +++ b/verification/verifast/start-vfide.sh @@ -18,6 +18,8 @@ TASKS_C="$SOURCE_DIR/tasks.c" PROOF_SETUP_DIR="proof_setup" GENERATED_HEADERS_DIR="$PROOF_SETUP_DIR/generated" +RP2040_CONFIG_DIR="$SOURCE_DIR/portable/ThirdParty/GCC/RP2040/include" + FREERTOS_SMP_DEMO_DIR="demos/FreeRTOS-SMP-Demos" PICO_SDK_DIR="sdks/pico-sdk" @@ -28,11 +30,12 @@ PICO_SDK_DIR="sdks/pico-sdk" # -> # `$GENERATED_HEADERS_DIR/pico_base` + + "$VFIDE" -I "$HEADER_DIR" \ -I $PROOF_SETUP_DIR -D VERIFAST "$TASKS_C" \ --I $FREERTOS_SMP_DEMO_DIR/FreeRTOS/Source/portable/ThirdParty/GCC/RP2040/include \ +-I $RP2040_CONFIG_DIR \ -I $PICO_SDK_DIR/src/common/pico_base/include \ --I $FREERTOS_SMP_DEMO_DIR/FreeRTOS/Source/include \ -I $GENERATED_HEADERS_DIR/pico_base \ -I $PICO_SDK_DIR/src/boards/include \ -I $PICO_SDK_DIR/src/rp2_common/cmsis/include \