coreboot-kgpe-d16/util/romcc/tests/simple_test81.c

static void main(void)
{
	int i;
	i = __builtin_inb(0x1234);
	int j;
	j = __builtin_inb(0xabcd);

}