#include <stdio.h>
extern int page_branch(void);
int main(int argc, char **argv)
{
    unsigned long next = ((unsigned long)page_branch & ~8191UL) + 8192UL;
    int result;
    if (argc > 1) {
        volatile unsigned short value = *(volatile unsigned short *)next;
        (void)value;
    }
    result = page_branch();
    printf("branch=%p next-page=%lx prefault=%d result=%d\n",
        (void *)page_branch, next, argc > 1, result);
    return result;
}