Made config macros from FreeRTOSConfig.h available to VeriFast proof.

tasks.c

@@ -30,6 +30,13 @@
      */
 
     //@ #include <bitops.gh>
+
+    /* The following includes will be visible to VeriFast in the preprocessed
+     * code. VeriFast requires includes to occur befor definitions. Hence,
+     * all includes visible to VeriFast must occur before the preprocessed
+     * ones. 
+     */
+    //VF_include #include "FreeRTOSConfig.h"
 #endif /* VERIFAST */
 
 

verification/verifast/custom_build_scripts_RP2040/vf_rewrite.sh

@@ -39,6 +39,9 @@ rewrite "__attribute__( ( [_a-z]* ) )" ""
 echo "Removing const qualifiers from pointers"
 rewrite "* const" "*"
 
+echo "Uncomment special includes to allow VeriFast proofs to refer to config macros"
+rewrite "//VF_include #include" "#include"
+
 #echo "VF RW: 'long unsigned int' -> 'unsinged long int'"
 #echo "backup : $VF_RW_WD/$SOURCE_FILE.backup-$BACKUP_IDX"
 #echo backup index $BACKUP_IDX

verification/verifast/proof/verifast_port_contracts.h

@@ -2,6 +2,19 @@
 #define VERIFAST_PORT_CONTRACTS_H
 
 
+// We want our proofs to hold for an arbitrary number of cores.
+/* TODO: Can we use the original function `get_core_num` instead without
+ *       adding the contract inside the pico sdk file (platform.h)?
+ */
+#undef portGET_CORE_ID
+#define portGET_CORE_ID() VF__get_core_num()
+
+/* FreeRTOS core id is always zero based.*/
+static uint VF__get_core_num(void);
+//@ requires true;
+//@ ensures result < configNUM_CORES;
+
+
 /*@ 
 predicate interruptState_p(uint32_t);
 

verification/verifast/start-vfide--preprocessed.sh

@@ -31,6 +31,7 @@ echo "\n\nPreprocessing script finished\n\n"
 # Remarks:
 # - Need z3v4.5 to handle bitvector arithmetic
 "$VF_DIR/bin/vfide" "$PP_TASK_C" \
+    -I proof_setup \
     -codeFont "$FONT_SIZE" -traceFont "$FONT_SIZE" \
     -prover z3v4.5
 #    -target 32bit -prover z3v4.5 \