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

Renamed VERIFAST_PROOF define into VERIFAST.

Browse source
This commit is contained in:
Tobias Reinhard 2022-10-11 15:32:57 -04:00
parent 7f69232893
commit 497a23d2eb
6 changed files with 7 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

2
tasks.c
View file

@ -25,7 +25,7 @@
*/ */
/* Verifast proof setup */ /* Verifast proof setup */
#ifdef VERIFAST_PROOF #ifdef VERIFAST
#include "verifast_proof_defs.h" #include "verifast_proof_defs.h"
#endif #endif

2
verification/verifast/proof_setup/generated/pico_base/pico/config_autogen.h
View file

@ -6,7 +6,7 @@
// based on PICO_CONFIG_HEADER_FILES: // based on PICO_CONFIG_HEADER_FILES:
#ifdef VERIFAST_PROOF #ifdef VERIFAST
/* Reason for rewrite: VeriFast cannot handle absolute include paths. */ /* Reason for rewrite: VeriFast cannot handle absolute include paths. */
#include "freertos_sdk_config.h" #include "freertos_sdk_config.h"
#include "boards/pico.h" #include "boards/pico.h"

2
verification/verifast/proof_setup/sys/cdefs.h
View file

@ -70,7 +70,7 @@
#define _CDEFS_H_ #define _CDEFS_H_
/* Verifast proof setup */ /* Verifast proof setup */
#ifdef VERIFAST_PROOF #ifdef VERIFAST
/* /*
* The proof setup header is already included at the top of the proof target, * The proof setup header is already included at the top of the proof target,
* e.g., `tasks.c`. But it seems like the contained defines are not propagated * e.g., `tasks.c`. But it seems like the contained defines are not propagated

4
verification/verifast/proof_setup/verifast_proof_defs.h
View file

@ -7,7 +7,7 @@
// /Users/reitobia/repos/forked/FreeRTOS-Kernel/verification/verifast/proof_setup_incremental/verifast_proof_defs.h // /Users/reitobia/repos/forked/FreeRTOS-Kernel/verification/verifast/proof_setup_incremental/verifast_proof_defs.h
#ifndef VERIFAST_PROOF_DEFS_H #ifndef VERIFAST_DEFS_H
// The following defines are required by `FRTOS.h` // The following defines are required by `FRTOS.h`
// line 93 // line 93
#define configMAX_PRIORITIES 100 #define configMAX_PRIORITIES 100
@ -21,4 +21,4 @@
#define __arm__ #define __arm__
#endif /* VERIFAST_PROOF_DEFS_H */ #endif /* VERIFAST_DEFS_H */

2
verification/verifast/sdks/pico-sdk

@ -1 +1 @@
Subproject commit 0c8802074d519ed0354400d85113c98618277c8b Subproject commit 649256491cc60f331d39d2d06def7da8ede91790

2
verification/verifast/start-vfide.sh
View file

@ -29,7 +29,7 @@ PICO_SDK_DIR="sdks/pico-sdk"
# `$GENERATED_HEADERS_DIR/pico_base` # `$GENERATED_HEADERS_DIR/pico_base`
"$VFIDE" -I "$HEADER_DIR" \ "$VFIDE" -I "$HEADER_DIR" \
-I $PROOF_SETUP_DIR -D VERIFAST_PROOF "$TASKS_C" \ -I $PROOF_SETUP_DIR -D VERIFAST "$TASKS_C" \
-I $FREERTOS_SMP_DEMO_DIR/FreeRTOS/Source/portable/ThirdParty/GCC/RP2040/include \ -I $FREERTOS_SMP_DEMO_DIR/FreeRTOS/Source/portable/ThirdParty/GCC/RP2040/include \
-I $PICO_SDK_DIR/src/common/pico_base/include \ -I $PICO_SDK_DIR/src/common/pico_base/include \
-I $FREERTOS_SMP_DEMO_DIR/FreeRTOS/Source/include \ -I $FREERTOS_SMP_DEMO_DIR/FreeRTOS/Source/include \