#include <stdio.h>
#include <stdint.h>
#include <inttypes.h>

uint64_t
foo(uint64_t a, uint64_t b);

int
main()
{
    uint64_t x = 3;
    uint64_t y = 4;

    uint64_t res = foo(x, y);

    printf("foo(%" PRIu64 ", %" PRIu64 ") returned %" PRIu64 "\n", x, y, res);
}