The problem: I want to apply the Polyspace bug finder with MISRA rules to a legacy project (toolchain not to be changed for now) running Zephyr RTOS on an STM32 ARM, but it does not compile the whole project. The libc headers used by Polyspace differ from the ones the GCC 8 (arm-none-eabi-gcc with C99) uses. My Polyspace 2020B does not let me select the correct compiler, and I don't find a place to add another toolchain. The closest I get is the following configuration.
The concrete symptom: The compiler reports the following error when compiling Zephyr:
File C:\[...]\zephyrproject\zephyr\include\net\socket_select.h line 118
Error: declaration is incompatible with "int select(int, fd_set *__restrict__, fd_set *__restrict__, fd_set *__restrict__, struct timeval *__restrict__)"
(declared at line 108 of "C:\[...]\Polyspace\R2020b\polyspace\verifier\cxx\include\include-libc\sys\select.h")
static inline int select(int nfds, zsock_fd_set *readfds,
The full declaration of select in Polyspace is:
extern int select (int __nfds, fd_set *__restrict __readfds,
fd_set *__restrict __writefds,
fd_set *__restrict __exceptfds,
struct timeval *__restrict __timeout);
In the ARM libc headers it is declared as (without restrict):
int select __P ((int __n, fd_set *__readfds, fd_set *__writefds,
fd_set *__exceptfds, struct timeval *__timeout));
The Zephyrproject actually implements it as follows:
#define fd_set zsock_fd_set
#define timeval zsock_timeval
#define FD_SETSIZE ZSOCK_FD_SETSIZE
static inline int select(int nfds, zsock_fd_set *readfds,
zsock_fd_set *writefds, zsock_fd_set *exceptfds,
struct timeval *timeout)
{
return zsock_select(nfds, readfds, writefds, exceptfds, timeout);
}
I would prefer solving it cleanly by just using the same compiler and libc as the original project does. However, as this is the only error message, I would also appreciate any workaround.
