#include <stdio.h>
#include <stdint.h>
char *__attribute__((section(".text"))) incr = "fhUUfhUUfhUUfhUUTZH+:H+:H+:ZWX\xc3";
int main() {
    uint64_t __attribute__((sysv_abi)) (* increment)(uint64_t) = (void *)incr;
    uint64_t x = 0x123456789abcdef;
    printf("inc(%lx) = %lx\n", x, increment(x));
    return 0;
}