PATCH] OS: Add some noreturn and printf compiler attributes where appropriate

[Mark Kettenis]

Given the fact that the "noreturn" attribute makes GCC generate code
that makes debugging hard (see the recent discussion about adding some
arm-specific compiler flags as a countermeasure), it's probably best
to keep its usage to the absolute minimum.