File ‹bugzilla180.c›
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
typedef unsigned int int32_t;
#define BIT(n) (1 << (n))
#define PAGE_BITS 12
#define PPTR_KDEV 0xffff0000
#define PPTR_APIC PPTR_KDEV
#define PPTR_DRHU_START (PPTR_APIC + BIT(PAGE_BITS))
#define MAX_NUM_DRHU ((-PPTR_DRHU_START) >> PAGE_BITS)
#define MAX_NUM_DRHU_VARIANT ((-(int32_t)PPTR_DRHU_START) >> PAGE_BITS)
char array[MAX_NUM_DRHU]; // array of 15 chars
char array2[MAX_NUM_DRHU_VARIANT]; // ditto
char f(unsigned i) { return i < 15 ? array[i] : 0; }
int g(void) { return sizeof(array); }
int h(void) { return sizeof(array2); }