#include <stdio.h>

static int cpu = 1;

static void schedule(void);

static int get_cpu(void) __attribute__((pure));

int main(void)
{
	int cpu1, cpu2, cpu3, cpu4;
	cpu1 = get_cpu();
	cpu2 = get_cpu();
	schedule();
	cpu3 = get_cpu();
	cpu4 = get_cpu();
	printf("the cpu values were %d %d %d %d.\n",
		cpu1, cpu2, cpu3, cpu4);
	return 0;
}

static int get_cpu(void)
{
	printf("get_cpu called.\n");
	return cpu;
}

static void schedule(void)
{
	cpu = 2;
	printf("schedule called .\n");
}