11590Srgrimes/*
21590Srgrimes * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
31590Srgrimes *
41590Srgrimes * SPDX-License-Identifier: BSD-2-Clause
51590Srgrimes */
61590Srgrimes
71590Srgrimestypedef unsigned int int32_t;
81590Srgrimes
91590Srgrimes#define BIT(n) (1 << (n))
101590Srgrimes#define PAGE_BITS 12
111590Srgrimes#define PPTR_KDEV 0xffff0000
121590Srgrimes#define PPTR_APIC PPTR_KDEV
131590Srgrimes#define PPTR_DRHU_START (PPTR_APIC + BIT(PAGE_BITS))
141590Srgrimes#define MAX_NUM_DRHU ((-PPTR_DRHU_START) >> PAGE_BITS)
151590Srgrimes#define MAX_NUM_DRHU_VARIANT ((-(int32_t)PPTR_DRHU_START) >> PAGE_BITS)
161590Srgrimes
171590Srgrimes
181590Srgrimes
191590Srgrimeschar array[MAX_NUM_DRHU];  // array of 15 chars
201590Srgrimeschar array2[MAX_NUM_DRHU_VARIANT]; // ditto
211590Srgrimes
221590Srgrimeschar f(unsigned i) { return i < 15 ? array[i] : 0; }
231590Srgrimes
241590Srgrimesint g(void) { return sizeof(array); }
251590Srgrimes
261590Srgrimesint h(void) { return sizeof(array2); }
271590Srgrimes