From 497a23d2ebddf1d8edb7a2b48e031dd9fc857e7d Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Tue, 11 Oct 2022 15:32:57 -0400
Subject: [PATCH] Renamed `VERIFAST_PROOF` define into `VERIFAST`.

---
 tasks.c                                                       | 2 +-
 .../proof_setup/generated/pico_base/pico/config_autogen.h     | 2 +-
 verification/verifast/proof_setup/sys/cdefs.h                 | 2 +-
 verification/verifast/proof_setup/verifast_proof_defs.h       | 4 ++--
 verification/verifast/sdks/pico-sdk                           | 2 +-
 verification/verifast/start-vfide.sh                          | 2 +-
 6 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/tasks.c b/tasks.c
index ff67e224f..1afc706e4 100644
--- a/tasks.c
+++ b/tasks.c
@@ -25,7 +25,7 @@
  */
  
 /* Verifast proof setup */
-#ifdef VERIFAST_PROOF
+#ifdef VERIFAST
     #include "verifast_proof_defs.h"
 #endif
 
diff --git a/verification/verifast/proof_setup/generated/pico_base/pico/config_autogen.h b/verification/verifast/proof_setup/generated/pico_base/pico/config_autogen.h
index 486e12e97..013a80dfc 100644
--- a/verification/verifast/proof_setup/generated/pico_base/pico/config_autogen.h
+++ b/verification/verifast/proof_setup/generated/pico_base/pico/config_autogen.h
@@ -6,7 +6,7 @@
 
 // based on PICO_CONFIG_HEADER_FILES:
 
-#ifdef VERIFAST_PROOF
+#ifdef VERIFAST
     /* Reason for rewrite: VeriFast cannot handle absolute include paths. */
     #include "freertos_sdk_config.h"
     #include "boards/pico.h"
diff --git a/verification/verifast/proof_setup/sys/cdefs.h b/verification/verifast/proof_setup/sys/cdefs.h
index e86eb4c13..0940dd633 100644
--- a/verification/verifast/proof_setup/sys/cdefs.h
+++ b/verification/verifast/proof_setup/sys/cdefs.h
@@ -70,7 +70,7 @@
 #define _CDEFS_H_
 
 /* Verifast proof setup */
-#ifdef VERIFAST_PROOF
+#ifdef VERIFAST
     /*
      * 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
diff --git a/verification/verifast/proof_setup/verifast_proof_defs.h b/verification/verifast/proof_setup/verifast_proof_defs.h
index 73f0578c5..77c2a9184 100644
--- a/verification/verifast/proof_setup/verifast_proof_defs.h
+++ b/verification/verifast/proof_setup/verifast_proof_defs.h
@@ -7,7 +7,7 @@
 // /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`
     // line 93
     #define configMAX_PRIORITIES 100
@@ -21,4 +21,4 @@
     #define __arm__
 
 
-#endif /* VERIFAST_PROOF_DEFS_H */
+#endif /* VERIFAST_DEFS_H */
diff --git a/verification/verifast/sdks/pico-sdk b/verification/verifast/sdks/pico-sdk
index 0c8802074..649256491 160000
--- a/verification/verifast/sdks/pico-sdk
+++ b/verification/verifast/sdks/pico-sdk
@@ -1 +1 @@
-Subproject commit 0c8802074d519ed0354400d85113c98618277c8b
+Subproject commit 649256491cc60f331d39d2d06def7da8ede91790
diff --git a/verification/verifast/start-vfide.sh b/verification/verifast/start-vfide.sh
index ba01278cc..a49fcd657 100755
--- a/verification/verifast/start-vfide.sh
+++ b/verification/verifast/start-vfide.sh
@@ -29,7 +29,7 @@ PICO_SDK_DIR="sdks/pico-sdk"
 # `$GENERATED_HEADERS_DIR/pico_base`
 
 "$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 $PICO_SDK_DIR/src/common/pico_base/include \
 -I $FREERTOS_SMP_DEMO_DIR/FreeRTOS/Source/include  \