#include <l4/macros.h>
#include <l4/config.h>
#include <l4/types.h>
#include INC_GLUE(memory.h)

unsigned int PAGE_SIZE = TEST_PAGE_SIZE;
unsigned int PAGE_MASK = TEST_PAGE_MASK;
unsigned int PAGE_BITS = TEST_PAGE_BITS;