#include <stdint.h>
uint32_t c_always_inlined() {
return 1234;
}
__attribute__((noinline)) uint32_t c_never_inlined() {
return 12345;