Compile a program with a third-party compiler and then integrate it with RIOT-OS

Help
1

Hello,

Can we compile a program with CompCert then integrate it with other RIOT-OS modules (compiled by GCC) and finally flash the result into a support board?

If so, how to do it?

For example, A helloWorld program

//bench_compcert/main.c
#include <stdio.h>
int main(void) {

    printf("HelloWorld\n");

    return 0;
}

Currently, when I do BOARD=nrf52840dk make -C tests/bench_compcert WERROR=0 flash, it uses default gcc to compile all used modules and my program. While I hope to

  • use GCC to compile RIOT-OS modules
  • use CompCert to compile my code

and then produce a .elf / .bin files…

A real-world case is that my program relies on some CompCert build-in functions, and I hope to run this program + RIOT-OS on my board.