[Xenomai] multiarch on ipipe kernel

[Frederik Bayart <frederik_bayart@yahoo.co.uk>]

Should it be possible to run an 32 bit non-rt binary on a 64 bit ipipe kernel ?
I'm using debian jessie amd64 and xenomai 2.6.4 on kernel 3.18.20

I have added i386 as foreing architecture and installed the i386 toolchain
$ dpkg --print-architectureamd64s$ dpkg --print-foreign-architecturesi386
I have a small hello world binary

#include <stdio.h>
int main(int argc, char* argv[]){  printf("hello world\n");  return 0;}
I compile with 
gcc -m32 -o hello hello.c
This binary runs on the normal (non-ipipe) kernel linux-image-3.16.0-4-amd64.But if I'm booting the ipipe kernel on the same system, I get the error :
-bash: ./hello: cannot execute binary file: Exec format error
So the problem seems to be related to the kernel. But I didn't find whether a kernel option could be the cause. The kernel was prepared with I only found that you can't run 32 bit xenomai libraries on a 64 bit kernel, but this binary is not using these libraries.
Kind regards,
Frederik