From 2c493715f40dc3d2848f3b618bbd70d11dd8d815 Mon Sep 17 00:00:00 2001 From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com> Date: Fri, 21 Oct 2022 10:56:47 -0400 Subject: [PATCH] Configured preprocessing script to process tasks.c file with verifast config. --- .../preprocess_tasks_c.sh | 4 +++- .../verifast/proof_setup/verifast_proof_defs.h | 17 +---------------- 2 files changed, 4 insertions(+), 17 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 37cebdf5e..df3c6796a 100755 --- a/verification/verifast/custom_build_scripts_RP2040/preprocess_tasks_c.sh +++ b/verification/verifast/custom_build_scripts_RP2040/preprocess_tasks_c.sh @@ -24,6 +24,8 @@ mkdir $LOG_PP_OUT_DIR clang -E -C -DFREE_RTOS_KERNEL_SMP=1 -DLIB_FREERTOS_KERNEL=1 -DLIB_PICO_BIT_OPS=1 -DLIB_PICO_BIT_OPS_PICO=1 -DLIB_PICO_DIVIDER=1 -DLIB_PICO_DIVIDER_HARDWARE=1 -DLIB_PICO_DOUBLE=1 -DLIB_PICO_DOUBLE_PICO=1 -DLIB_PICO_FLOAT=1 -DLIB_PICO_FLOAT_PICO=1 -DLIB_PICO_INT64_OPS=1 -DLIB_PICO_INT64_OPS_PICO=1 -DLIB_PICO_MALLOC=1 -DLIB_PICO_MEM_OPS=1 -DLIB_PICO_MEM_OPS_PICO=1 -DLIB_PICO_MULTICORE=1 -DLIB_PICO_PLATFORM=1 -DLIB_PICO_PRINTF=1 -DLIB_PICO_PRINTF_PICO=1 -DLIB_PICO_RUNTIME=1 -DLIB_PICO_STANDARD_LINK=1 -DLIB_PICO_STDIO=1 -DLIB_PICO_STDIO_UART=1 -DLIB_PICO_STDLIB=1 -DLIB_PICO_SYNC=1 -DLIB_PICO_SYNC_CORE=1 -DLIB_PICO_SYNC_CRITICAL_SECTION=1 -DLIB_PICO_SYNC_MUTEX=1 -DLIB_PICO_SYNC_SEM=1 -DLIB_PICO_TIME=1 -DLIB_PICO_UTIL=1 -DPICO_BOARD=\"pico\" -DPICO_BUILD=1 -DPICO_CMAKE_BUILD_TYPE=\"Release\" -DPICO_COPY_TO_RAM=0 -DPICO_CXX_ENABLE_EXCEPTIONS=0 -DPICO_NO_FLASH=0 -DPICO_NO_HARDWARE=0 -DPICO_ON_DEVICE=1 -DPICO_STACK_SIZE=0x1000 -DPICO_TARGET_NAME=\"on_core_one\" -DPICO_USE_BLOCKED_RAM=0 -DmainRUN_FREE_RTOS_ON_CORE=1 \ +-DVERIFAST \ +-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 \ @@ -66,7 +68,7 @@ clang -E -C -DFREE_RTOS_KERNEL_SMP=1 -DLIB_FREERTOS_KERNEL=1 -DLIB_PICO_BIT_OPS -I/Users/reitobia/programs/pico-sdk/src/common/pico_binary_info/include \ -I/Users/reitobia/programs/pico-sdk/src/rp2_common/pico_stdio/include \ -I/Users/reitobia/programs/pico-sdk/src/rp2_common/pico_stdio_uart/include \ --c /Users/reitobia/repos2/FreeRTOS-Kernel/verification/verifast/demos/FreeRTOS-SMP-Demos/FreeRTOS/Source/tasks.c \ +-c /Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c \ &>$LOG_PP_TASK_C echo "\n\nPreprocessed output with pragmas written to:" diff --git a/verification/verifast/proof_setup/verifast_proof_defs.h b/verification/verifast/proof_setup/verifast_proof_defs.h index 77c2a9184..61aa629c7 100644 --- a/verification/verifast/proof_setup/verifast_proof_defs.h +++ b/verification/verifast/proof_setup/verifast_proof_defs.h @@ -1,24 +1,9 @@ /* - * This file contains defines to configure the VeriFast proof setup which are - * not already handled in `port.c` or `portmacro.h`. + * This file contains defines to configure the VeriFast proof setup. * */ -// /Users/reitobia/repos/forked/FreeRTOS-Kernel/verification/verifast/proof_setup_incremental/verifast_proof_defs.h - #ifndef VERIFAST_DEFS_H - // The following defines are required by `FRTOS.h` - // line 93 - #define configMAX_PRIORITIES 100 - - // The following defines are required by `cdefs.h` - #define __GNUC__ 10 - #define __STDC__ 1 - - // line 827 - // This proof setup assumes an RP2040 processor (Raspberry Pi Pico). - #define __arm__ - #endif /* VERIFAST_DEFS_H */