mirror of
https://github.com/FreeRTOS/FreeRTOS-Kernel.git
synced 2025-12-12 06:35:19 -05:00
Resolved VF parse error in pico sdk's platform.h and deleted stub.
This commit is contained in:
Tobias Reinhard
parent
e652475628
commit
7f69232893
4 changed files with 2 additions and 508 deletions
|
|
@ -1,2 +0,0 @@
|
||||||
This directory contains files that originally resided in:
|
|
||||||
`$PICO_SDK_PATH/src/rp2_common/pico_platform/include/pico`
|
|
||||||
|
|
@ -1,504 +0,0 @@
|
||||||
/* This is a stub used for the VeriFast proof. */
|
|
||||||
/*
|
|
||||||
* Copyright (c) 2020 Raspberry Pi (Trading) Ltd.
|
|
||||||
*
|
|
||||||
* SPDX-License-Identifier: BSD-3-Clause
|
|
||||||
*/
|
|
||||||
|
|
||||||
#ifndef _PICO_PLATFORM_H_
|
|
||||||
#define _PICO_PLATFORM_H_
|
|
||||||
|
|
||||||
/** \file platform.h
|
|
||||||
* \defgroup pico_platform pico_platform
|
|
||||||
*
|
|
||||||
* Macros and definitions (and functions when included by non assembly code) for the RP2 family device / architecture
|
|
||||||
* to provide a common abstraction over low level compiler / platform specifics.
|
|
||||||
*
|
|
||||||
* This header may be included by assembly code
|
|
||||||
*/
|
|
||||||
|
|
||||||
#include "hardware/platform_defs.h"
|
|
||||||
#include "hardware/regs/addressmap.h"
|
|
||||||
#include "hardware/regs/sio.h"
|
|
||||||
|
|
||||||
// Marker for builds targeting the RP2040
|
|
||||||
#define PICO_RP2040 1
|
|
||||||
|
|
||||||
// PICO_CONFIG: PICO_STACK_SIZE, Stack Size, min=0x100, default=0x800, advanced=true, group=pico_platform
|
|
||||||
#ifndef PICO_STACK_SIZE
|
|
||||||
#define PICO_STACK_SIZE _u(0x800)
|
|
||||||
#endif
|
|
||||||
|
|
||||||
// PICO_CONFIG: PICO_HEAP_SIZE, Heap size to reserve, min=0x100, default=0x800, advanced=true, group=pico_platform
|
|
||||||
#ifndef PICO_HEAP_SIZE
|
|
||||||
#define PICO_HEAP_SIZE _u(0x800)
|
|
||||||
#endif
|
|
||||||
|
|
||||||
// PICO_CONFIG: PICO_NO_RAM_VECTOR_TABLE, Enable/disable the RAM vector table, type=bool, default=0, advanced=true, group=pico_platform
|
|
||||||
#ifndef PICO_NO_RAM_VECTOR_TABLE
|
|
||||||
#define PICO_NO_RAM_VECTOR_TABLE 0
|
|
||||||
#endif
|
|
||||||
|
|
||||||
// PICO_CONFIG: PICO_RP2040_B0_SUPPORTED, Whether to include any specific software support for RP2040 B0 revision, type=bool, default=1, advanced=true, group=pico_platform
|
|
||||||
#ifndef PICO_RP2040_B0_SUPPORTED
|
|
||||||
#define PICO_RP2040_B0_SUPPORTED 1
|
|
||||||
#endif
|
|
||||||
|
|
||||||
// PICO_CONFIG: PICO_FLOAT_SUPPORT_ROM_V1, Include float support code for RP2040 B0 when that chip revision is supported , type=bool, default=1, advanced=true, group=pico_platform
|
|
||||||
#ifndef PICO_FLOAT_SUPPORT_ROM_V1
|
|
||||||
#define PICO_FLOAT_SUPPORT_ROM_V1 1
|
|
||||||
#endif
|
|
||||||
|
|
||||||
// PICO_CONFIG: PICO_DOUBLE_SUPPORT_ROM_V1, Include double support code for RP2040 B0 when that chip revision is supported , type=bool, default=1, advanced=true, group=pico_platform
|
|
||||||
#ifndef PICO_DOUBLE_SUPPORT_ROM_V1
|
|
||||||
#define PICO_DOUBLE_SUPPORT_ROM_V1 1
|
|
||||||
#endif
|
|
||||||
|
|
||||||
|
|
||||||
// PICO_CONFIG: PICO_RP2040_B1_SUPPORTED, Whether to include any specific software support for RP2040 B1 revision, type=bool, default=1, advanced=true, group=pico_platform
|
|
||||||
#ifndef PICO_RP2040_B1_SUPPORTED
|
|
||||||
#define PICO_RP2040_B1_SUPPORTED 1
|
|
||||||
#endif
|
|
||||||
|
|
||||||
// PICO_CONFIG: PICO_RP2040_B2_SUPPORTED, Whether to include any specific software support for RP2040 B2 revision, type=bool, default=1, advanced=true, group=pico_platform
|
|
||||||
#ifndef PICO_RP2040_B2_SUPPORTED
|
|
||||||
#define PICO_RP2040_B2_SUPPORTED 1
|
|
||||||
#endif
|
|
||||||
|
|
||||||
// --- remainder of file is not included by assembly code ---
|
|
||||||
|
|
||||||
#ifndef __ASSEMBLER__
|
|
||||||
|
|
||||||
#include <sys/cdefs.h>
|
|
||||||
#include "pico/types.h"
|
|
||||||
|
|
||||||
#ifdef __cplusplus
|
|
||||||
extern "C" {
|
|
||||||
#endif
|
|
||||||
|
|
||||||
/*! \brief Marker for an interrupt handler
|
|
||||||
* \ingroup pico_platform
|
|
||||||
* For example an IRQ handler function called my_interrupt_handler:
|
|
||||||
*
|
|
||||||
* void __isr my_interrupt_handler(void) {
|
|
||||||
*/
|
|
||||||
#define __isr
|
|
||||||
|
|
||||||
/*! \brief Section attribute macro for placement in RAM after the `.data` section
|
|
||||||
* \ingroup pico_platform
|
|
||||||
*
|
|
||||||
* For example a 400 element `uint32_t` array placed after the .data section
|
|
||||||
*
|
|
||||||
* uint32_t __after_data("my_group_name") a_big_array[400];
|
|
||||||
*
|
|
||||||
* The section attribute is `.after_data.<group>`
|
|
||||||
*
|
|
||||||
* \param group a string suffix to use in the section name to distinguish groups that can be linker
|
|
||||||
* garbage-collected independently
|
|
||||||
*/
|
|
||||||
#define __after_data(group) __attribute__((section(".after_data." group)))
|
|
||||||
|
|
||||||
/*! \brief Section attribute macro for placement not in flash (i.e in RAM)
|
|
||||||
* \ingroup pico_platform
|
|
||||||
*
|
|
||||||
* For example a 3 element `uint32_t` array placed in RAM (even though it is `static const`)
|
|
||||||
*
|
|
||||||
* static const uint32_t __not_in_flash("my_group_name") an_array[3];
|
|
||||||
*
|
|
||||||
* The section attribute is `.time_critical.<group>`
|
|
||||||
*
|
|
||||||
* \param group a string suffix to use in the section name to distinguish groups that can be linker
|
|
||||||
* garbage-collected independently
|
|
||||||
*/
|
|
||||||
#define __not_in_flash(group) __attribute__((section(".time_critical." group)))
|
|
||||||
|
|
||||||
/*! \brief Section attribute macro for placement in the SRAM bank 4 (known as "scratch X")
|
|
||||||
* \ingroup pico_platform
|
|
||||||
*
|
|
||||||
* Scratch X is commonly used for critical data and functions accessed only by one core (when only
|
|
||||||
* one core is accessing the RAM bank, there is no opportunity for stalls)
|
|
||||||
*
|
|
||||||
* For example a `uint32_t` variable placed in "scratch X"
|
|
||||||
*
|
|
||||||
* uint32_t __scratch_x("my_group_name") foo = 23;
|
|
||||||
*
|
|
||||||
* The section attribute is `.scratch_x.<group>`
|
|
||||||
*
|
|
||||||
* \param group a string suffix to use in the section name to distinguish groups that can be linker
|
|
||||||
* garbage-collected independently
|
|
||||||
*/
|
|
||||||
#define __scratch_x(group) __attribute__((section(".scratch_x." group)))
|
|
||||||
|
|
||||||
/*! \brief Section attribute macro for placement in the SRAM bank 5 (known as "scratch Y")
|
|
||||||
* \ingroup pico_platform
|
|
||||||
*
|
|
||||||
* Scratch Y is commonly used for critical data and functions accessed only by one core (when only
|
|
||||||
* one core is accessing the RAM bank, there is no opportunity for stalls)
|
|
||||||
*
|
|
||||||
* For example a `uint32_t` variable placed in "scratch Y"
|
|
||||||
*
|
|
||||||
* uint32_t __scratch_y("my_group_name") foo = 23;
|
|
||||||
*
|
|
||||||
* The section attribute is `.scratch_y.<group>`
|
|
||||||
*
|
|
||||||
* \param group a string suffix to use in the section name to distinguish groups that can be linker
|
|
||||||
* garbage-collected independently
|
|
||||||
*/
|
|
||||||
#define __scratch_y(group) __attribute__((section(".scratch_y." group)))
|
|
||||||
|
|
||||||
/*! \brief Section attribute macro for data that is to be left uninitialized
|
|
||||||
* \ingroup pico_platform
|
|
||||||
*
|
|
||||||
* Data marked this way will retain its value across a reset (normally uninitialized data - in the .bss
|
|
||||||
* section) is initialized to zero during runtime initialization
|
|
||||||
*
|
|
||||||
* For example a `uint32_t` foo that will retain its value if the program is restarted by reset.
|
|
||||||
*
|
|
||||||
* uint32_t __uninitialized_ram("my_group_name") foo;
|
|
||||||
*
|
|
||||||
* The section attribute is `.uninitialized_ram.<group>`
|
|
||||||
*
|
|
||||||
* \param group a string suffix to use in the section name to distinguish groups that can be linker
|
|
||||||
* garbage-collected independently
|
|
||||||
*/
|
|
||||||
#define __uninitialized_ram(group) __attribute__((section(".uninitialized_ram." #group))) group
|
|
||||||
|
|
||||||
/*! \brief Section attribute macro for placement in flash even in a COPY_TO_RAM binary
|
|
||||||
* \ingroup pico_platform
|
|
||||||
*
|
|
||||||
* For example a `uint32_t` variable explicitly placed in flash (it will hard fault if you attempt to write it!)
|
|
||||||
*
|
|
||||||
* uint32_t __in_flash("my_group_name") foo = 23;
|
|
||||||
*
|
|
||||||
* The section attribute is `.flashdata.<group>`
|
|
||||||
*
|
|
||||||
* \param group a string suffix to use in the section name to distinguish groups that can be linker
|
|
||||||
* garbage-collected independently
|
|
||||||
*/
|
|
||||||
#define __in_flash(group) __attribute__((section(".flashdata" group)))
|
|
||||||
|
|
||||||
/*! \brief Indicates a function should not be stored in flash
|
|
||||||
* \ingroup pico_platform
|
|
||||||
*
|
|
||||||
* Decorates a function name, such that the function will execute from RAM (assuming it is not inlined
|
|
||||||
* into a flash function by the compiler)
|
|
||||||
*
|
|
||||||
* For example a function called my_func taking an int parameter:
|
|
||||||
*
|
|
||||||
* void __not_in_flash_func(my_func)(int some_arg) {
|
|
||||||
*
|
|
||||||
* The function is placed in the `.time_critical.<func_name>` linker section
|
|
||||||
*
|
|
||||||
* \see __no_inline_not_in_flash_func
|
|
||||||
*/
|
|
||||||
#define __not_in_flash_func(func_name) __not_in_flash(__STRING(func_name)) func_name
|
|
||||||
|
|
||||||
/*! \brief Indicates a function is time/latency critical and should not run from flash
|
|
||||||
* \ingroup pico_platform
|
|
||||||
*
|
|
||||||
* Decorates a function name, such that the function will execute from RAM (assuming it is not inlined
|
|
||||||
* into a flash function by the compiler) to avoid possible flash latency. Currently this macro is identical
|
|
||||||
* in implementation to `__not_in_flash_func`, however the semantics are distinct and a `__time_critical_func`
|
|
||||||
* may in the future be treated more specially to reduce the overhead when calling such function from a flash
|
|
||||||
* function.
|
|
||||||
*
|
|
||||||
* For example a function called my_func taking an int parameter:
|
|
||||||
*
|
|
||||||
* void __time_critical(my_func)(int some_arg) {
|
|
||||||
*
|
|
||||||
* The function is placed in the `.time_critical.<func_name>` linker section
|
|
||||||
*
|
|
||||||
* \see __not_in_flash_func
|
|
||||||
*/
|
|
||||||
#define __time_critical_func(func_name) __not_in_flash_func(func_name)
|
|
||||||
|
|
||||||
/*! \brief Indicate a function should not be stored in flash and should not be inlined
|
|
||||||
* \ingroup pico_platform
|
|
||||||
*
|
|
||||||
* Decorates a function name, such that the function will execute from RAM, explicitly marking it as
|
|
||||||
* noinline to prevent it being inlined into a flash function by the compiler
|
|
||||||
*
|
|
||||||
* For example a function called my_func taking an int parameter:
|
|
||||||
*
|
|
||||||
* void __no_inline_not_in_flash_func(my_func)(int some_arg) {
|
|
||||||
*
|
|
||||||
* The function is placed in the `.time_critical.<func_name>` linker section
|
|
||||||
*/
|
|
||||||
#define __no_inline_not_in_flash_func(func_name) __noinline __not_in_flash_func(func_name)
|
|
||||||
|
|
||||||
#define __packed_aligned __packed __aligned(4)
|
|
||||||
|
|
||||||
#ifdef VERIFAST_PROOF
|
|
||||||
/* Reason for rewrite:
|
|
||||||
* VeriFast cannot handle defines for `__force_inline`.
|
|
||||||
*/
|
|
||||||
#else
|
|
||||||
/*! \brief Attribute to force inlining of a function regardless of optimization level
|
|
||||||
* \ingroup pico_platform
|
|
||||||
*
|
|
||||||
* For example my_function here will always be inlined:
|
|
||||||
*
|
|
||||||
* int __force_inline my_function(int x) {
|
|
||||||
*
|
|
||||||
*/
|
|
||||||
#if defined(__GNUC__) && (__GNUC__ <= 6 || (__GNUC__ == 7 && (__GNUC_MINOR__ < 3 || !defined(__cplusplus))))
|
|
||||||
#define __force_inline inline __always_inline
|
|
||||||
#else
|
|
||||||
#define __force_inline __always_inline
|
|
||||||
#endif
|
|
||||||
#endif /* VERIFAST_PROOF */
|
|
||||||
|
|
||||||
/*! \brief Macro to determine the number of elements in an array
|
|
||||||
* \ingroup pico_platform
|
|
||||||
*/
|
|
||||||
#ifndef count_of
|
|
||||||
#define count_of(a) (sizeof(a)/sizeof((a)[0]))
|
|
||||||
#endif
|
|
||||||
|
|
||||||
/*! \brief Macro to return the maximum of two comparable values
|
|
||||||
* \ingroup pico_platform
|
|
||||||
*/
|
|
||||||
#ifndef MAX
|
|
||||||
#define MAX(a, b) ((a)>(b)?(a):(b))
|
|
||||||
#endif
|
|
||||||
|
|
||||||
/*! \brief Macro to return the minimum of two comparable values
|
|
||||||
* \ingroup pico_platform
|
|
||||||
*/
|
|
||||||
#ifndef MIN
|
|
||||||
#define MIN(a, b) ((b)>(a)?(a):(b))
|
|
||||||
#endif
|
|
||||||
|
|
||||||
/*! \brief Execute a breakpoint instruction
|
|
||||||
* \ingroup pico_platform
|
|
||||||
*/
|
|
||||||
static inline void __breakpoint(void) {
|
|
||||||
__asm__("bkpt #0");
|
|
||||||
}
|
|
||||||
|
|
||||||
/*! \brief Ensure that the compiler does not move memory access across this method call
|
|
||||||
* \ingroup pico_platform
|
|
||||||
*
|
|
||||||
* For example in the following code:
|
|
||||||
*
|
|
||||||
* *some_memory_location = var_a;
|
|
||||||
* __compiler_memory_barrier();
|
|
||||||
* uint32_t var_b = *some_other_memory_location
|
|
||||||
*
|
|
||||||
* The compiler will not move the load from `some_other_memory_location` above the memory barrier (which it otherwise
|
|
||||||
* might - even above the memory store!)
|
|
||||||
*/
|
|
||||||
#ifdef VERIFAST_PROOF
|
|
||||||
/* Reason for rewrite: VeriFast cannot parse:
|
|
||||||
* - `__force_inline`
|
|
||||||
* - the function body
|
|
||||||
*/
|
|
||||||
static void __compiler_memory_barrier(void);
|
|
||||||
#else
|
|
||||||
__force_inline static void __compiler_memory_barrier(void) {
|
|
||||||
__asm__ volatile ("" : : : "memory");
|
|
||||||
}
|
|
||||||
#endif
|
|
||||||
|
|
||||||
|
|
||||||
/*! \brief Macro for converting memory addresses to 32 bit addresses suitable for DMA
|
|
||||||
* \ingroup pico_platform
|
|
||||||
*
|
|
||||||
* This is just a cast to `uintptr_t` on the RP2040, however you may want to use this when developing code
|
|
||||||
* that also runs in "host" mode. If the host mode is 64 bit and you are embedding data pointers
|
|
||||||
* in other data (e.g. DMA chaining), then there is a need in "host" mode to convert a 64 bit native
|
|
||||||
* pointer to a 32 bit value for storage, which can be done using this macro.
|
|
||||||
*/
|
|
||||||
#define host_safe_hw_ptr(x) ((uintptr_t)(x))
|
|
||||||
#define native_safe_hw_ptr(x) host_safe_hw_ptr(x)
|
|
||||||
|
|
||||||
|
|
||||||
/*! \brief Panics with the message "Unsupported"
|
|
||||||
* \ingroup pico_platform
|
|
||||||
* \see panic
|
|
||||||
*/
|
|
||||||
#ifdef VERIFAST_PROOF
|
|
||||||
/* Reason for rewrite: VeriFast cannot parse `__attribute__((noreturn))`. */
|
|
||||||
void panic_unsupported(void);
|
|
||||||
#else
|
|
||||||
void __attribute__((noreturn)) panic_unsupported(void);
|
|
||||||
#endif
|
|
||||||
|
|
||||||
/*! \brief Displays a panic message and halts execution
|
|
||||||
* \ingroup pico_platform
|
|
||||||
*
|
|
||||||
* An attempt is made to output the message to all registered STDOUT drivers
|
|
||||||
* after which this method executes a BKPT instruction.
|
|
||||||
*
|
|
||||||
* @param fmt format string (printf-like)
|
|
||||||
* @param ... printf-like arguments
|
|
||||||
*/
|
|
||||||
#ifdef VERIFAST_PROOF
|
|
||||||
/* Reason for rewrite: VeriFast cannot parse `__attribute__((noreturn))`. */
|
|
||||||
void panic(const char *fmt, ...);
|
|
||||||
#else
|
|
||||||
void __attribute__((noreturn)) panic(const char *fmt, ...);
|
|
||||||
#endif
|
|
||||||
|
|
||||||
// PICO_CONFIG: PICO_NO_FPGA_CHECK, Remove the FPGA platform check for small code size reduction, type=bool, default=0, advanced=true, group=pico_runtime
|
|
||||||
#ifndef PICO_NO_FPGA_CHECK
|
|
||||||
#define PICO_NO_FPGA_CHECK 0
|
|
||||||
#endif
|
|
||||||
|
|
||||||
#if PICO_NO_FPGA_CHECK
|
|
||||||
static inline bool running_on_fpga(void) {return false;}
|
|
||||||
#else
|
|
||||||
bool running_on_fpga(void);
|
|
||||||
#endif
|
|
||||||
|
|
||||||
/*! \brief Returns the RP2040 chip revision number
|
|
||||||
* \ingroup pico_platform
|
|
||||||
* @return the RP2040 chip revision number (1 for B0/B1, 2 for B2)
|
|
||||||
*/
|
|
||||||
uint8_t rp2040_chip_version(void);
|
|
||||||
|
|
||||||
/*! \brief Returns the RP2040 rom version number
|
|
||||||
* \ingroup pico_platform
|
|
||||||
* @return the RP2040 rom version number (1 for RP2040-B0, 2 for RP2040-B1, 3 for RP2040-B2)
|
|
||||||
*/
|
|
||||||
static inline uint8_t rp2040_rom_version(void) {
|
|
||||||
#ifdef VERIFAST_PROOF
|
|
||||||
/* Reason for rewrite: VeriFast cannot parse GCC pragmas */
|
|
||||||
return *(uint8_t*)0x13;
|
|
||||||
#else
|
|
||||||
#pragma GCC diagnostic push
|
|
||||||
#pragma GCC diagnostic ignored "-Warray-bounds"
|
|
||||||
return *(uint8_t*)0x13;
|
|
||||||
#pragma GCC diagnostic pop
|
|
||||||
#endif /* VERIFAST_PROOF */
|
|
||||||
}
|
|
||||||
|
|
||||||
/*! \brief No-op function for the body of tight loops
|
|
||||||
* \ingroup pico_platform
|
|
||||||
*
|
|
||||||
* No-op function intended to be called by any tight hardware polling loop. Using this ubiquitously
|
|
||||||
* makes it much easier to find tight loops, but also in the future \#ifdef-ed support for lockup
|
|
||||||
* debugging might be added
|
|
||||||
*/
|
|
||||||
#ifdef VERIFAST_PROOF
|
|
||||||
/* Reason for rewrite: VeriFast cannot parse `__force_inline`. */
|
|
||||||
static void tight_loop_contents(void) {}
|
|
||||||
#else
|
|
||||||
static __force_inline void tight_loop_contents(void) {}
|
|
||||||
#endif /* VERIFAST_PROOF */
|
|
||||||
|
|
||||||
|
|
||||||
/*! \brief Multiply two integers using an assembly `MUL` instruction
|
|
||||||
* \ingroup pico_platform
|
|
||||||
*
|
|
||||||
* This multiplies a by b using multiply instruction using the ARM mul instruction regardless of values (the compiler
|
|
||||||
* might otherwise choose to perform shifts/adds), i.e. this is a 1 cycle operation.
|
|
||||||
*
|
|
||||||
* \param a the first operand
|
|
||||||
* \param b the second operand
|
|
||||||
* \return a * b
|
|
||||||
*/
|
|
||||||
#ifdef VERIFAST_PROOF
|
|
||||||
/* Reason for rewrite: VeriFast cannot parse:
|
|
||||||
* - `__force_inline`
|
|
||||||
* - function body
|
|
||||||
*/
|
|
||||||
static int32_t __mul_instruction(int32_t a, int32_t b);
|
|
||||||
#else
|
|
||||||
__force_inline static int32_t __mul_instruction(int32_t a, int32_t b) {
|
|
||||||
asm ("mul %0, %1" : "+l" (a) : "l" (b) : );
|
|
||||||
return a;
|
|
||||||
}
|
|
||||||
#endif /* VERIFAST_PROOF */
|
|
||||||
|
|
||||||
/*! \brief multiply two integer values using the fastest method possible
|
|
||||||
* \ingroup pico_platform
|
|
||||||
*
|
|
||||||
* Efficiently multiplies value a by possibly constant value b.
|
|
||||||
*
|
|
||||||
* If b is known to be constant and not zero or a power of 2, then a mul instruction is used rather than gcc's default
|
|
||||||
* which is often a slow combination of shifts and adds. If b is a power of 2 then a single shift is of course preferable
|
|
||||||
* and will be used
|
|
||||||
*
|
|
||||||
* \param a the first operand
|
|
||||||
* \param b the second operand
|
|
||||||
* \return a * b
|
|
||||||
*/
|
|
||||||
#define __fast_mul(a, b) __builtin_choose_expr(__builtin_constant_p(b) && !__builtin_constant_p(a), \
|
|
||||||
(__builtin_popcount(b) >= 2 ? __mul_instruction(a,b) : (a)*(b)), \
|
|
||||||
(a)*(b))
|
|
||||||
|
|
||||||
/*! \brief Utility macro to assert two types are equivalent.
|
|
||||||
* \ingroup pico_platform
|
|
||||||
*
|
|
||||||
* This macro can be useful in other macros along with `typeof` to assert that two parameters are of equivalent type
|
|
||||||
* (or that a single parameter is of an expected type)
|
|
||||||
*/
|
|
||||||
#define __check_type_compatible(type_a, type_b) static_assert(__builtin_types_compatible_p(type_a, type_b), __STRING(type_a) " is not compatible with " __STRING(type_b));
|
|
||||||
|
|
||||||
/*! \brief Get the current exception level on this core
|
|
||||||
* \ingroup pico_platform
|
|
||||||
*
|
|
||||||
* \return the exception number if the CPU is handling an exception, or 0 otherwise
|
|
||||||
*/
|
|
||||||
uint __get_current_exception(void);
|
|
||||||
|
|
||||||
#define WRAPPER_FUNC(x) __wrap_ ## x
|
|
||||||
#define REAL_FUNC(x) __real_ ## x
|
|
||||||
|
|
||||||
#ifdef __cplusplus
|
|
||||||
}
|
|
||||||
#endif
|
|
||||||
|
|
||||||
/*! \brief Helper method to busy-wait for at least the given number of cycles
|
|
||||||
* \ingroup pico_platform
|
|
||||||
*
|
|
||||||
* This method is useful for introducing very short delays.
|
|
||||||
*
|
|
||||||
* This method busy-waits in a tight loop for the given number of system clock cycles. The total wait time is only accurate to within 2 cycles,
|
|
||||||
* and this method uses a loop counter rather than a hardware timer, so the method will always take longer than expected if an
|
|
||||||
* interrupt is handled on the calling core during the busy-wait; you can of course disable interrupts to prevent this.
|
|
||||||
*
|
|
||||||
* You can use \ref clock_get_hz(clk_sys) to determine the number of clock cycles per second if you want to convert an actual
|
|
||||||
* time duration to a number of cycles.
|
|
||||||
*
|
|
||||||
* \param minimum_cycles the minimum number of system clock cycles to delay for
|
|
||||||
*/
|
|
||||||
#ifdef VERIFAST_PROOF
|
|
||||||
/* Reason for rewrite: VeriFast cannot parse function body. */
|
|
||||||
static inline void busy_wait_at_least_cycles(uint32_t minimum_cycles);
|
|
||||||
#else
|
|
||||||
static inline void busy_wait_at_least_cycles(uint32_t minimum_cycles) {
|
|
||||||
__asm volatile (
|
|
||||||
".syntax unified\n"
|
|
||||||
"1: subs %0, #3\n"
|
|
||||||
"bcs 1b\n"
|
|
||||||
: "+r" (minimum_cycles) : : "memory"
|
|
||||||
);
|
|
||||||
}
|
|
||||||
#endif /* VERIFAST_PROOF */
|
|
||||||
|
|
||||||
/*! \brief Get the current core number
|
|
||||||
* \ingroup pico_platform
|
|
||||||
*
|
|
||||||
* \return The core number the call was made from
|
|
||||||
*/
|
|
||||||
#ifdef VERIFAST_PROOF
|
|
||||||
/* Reason for rewrite: VeriFast cannot parse `__force_inline`. */
|
|
||||||
static uint get_core_num(void)
|
|
||||||
#else
|
|
||||||
__force_inline static uint get_core_num(void)
|
|
||||||
#endif /* VERIFAST_PROOF */
|
|
||||||
{
|
|
||||||
return (*(uint32_t *) (SIO_BASE + SIO_CPUID_OFFSET));
|
|
||||||
}
|
|
||||||
|
|
||||||
#else // __ASSEMBLER__
|
|
||||||
|
|
||||||
#define WRAPPER_FUNC_NAME(x) __wrap_##x
|
|
||||||
#define SECTION_NAME(x) .text.##x
|
|
||||||
#define RAM_SECTION_NAME(x) .time_critical.##x
|
|
||||||
|
|
||||||
#endif // !__ASSEMBLER__
|
|
||||||
|
|
||||||
#endif
|
|
||||||
|
|
@ -1 +1 @@
|
||||||
Subproject commit 2e6142b15b8a75c1227dd3edbe839193b2bf9041
|
Subproject commit 0c8802074d519ed0354400d85113c98618277c8b
|
||||||
|
|
@ -80,7 +80,7 @@ PICO_SDK_DIR="sdks/pico-sdk"
|
||||||
-I $PICO_SDK_DIR/src/rp2_common/pico_unique_id/include \
|
-I $PICO_SDK_DIR/src/rp2_common/pico_unique_id/include \
|
||||||
-I $PICO_SDK_DIR/src/rp2_common/hardware_flash/include \
|
-I $PICO_SDK_DIR/src/rp2_common/hardware_flash/include \
|
||||||
-I $PICO_SDK_DIR/src/common/pico_usb_reset_interface/include \
|
-I $PICO_SDK_DIR/src/common/pico_usb_reset_interface/include \
|
||||||
|
-I $PICO_SDK_DIR/src/rp2_common/pico_platform/include/
|
||||||
|
|
||||||
# Defines used during the built of the FreeRTOS SMP Demo that might be relevant
|
# Defines used during the built of the FreeRTOS SMP Demo that might be relevant
|
||||||
# in the future:
|
# in the future:
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue