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


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

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


    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.