Reported-by: Jorge Ramirez Ortiz <jro@xenomai.org> Debugged-by: Jorge Ramirez Ortiz <jro@xenomai.org>