Resolve some existing compiler warnings

[axel-h]

I was wondering if changing kernel/libsel4/include/sel4/functions.h to have

LIBSEL4_INLINE_FUNC void seL4_SetIPCBuffer(seL4_IPCBuffer *ipc_buffer) LIBSEL4_ATTRIBUTES_SetIPCBuffer
{
    __sel4_ipc_buffer = ipc_buffer;
    return;
}

and then just setting

#define LIBSEL4_ATTRIBUTES_SetIPCBuffer __attribute__((no_instrument_function))

might be a better approach to avoid redundancy. But I'm not really sure it this is better to understand without a few comments why this is needed.

[kent-mcleod]

I don't think it's worth complicating the original definition just to make it easier for this file to do something non-standard.