1/* 2 * Copyright 2017, Data61 3 * Commonwealth Scientific and Industrial Research Organisation (CSIRO) 4 * ABN 41 687 119 230. 5 * 6 * This software may be distributed and modified according to the terms of 7 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 8 * See "LICENSE_BSD2.txt" for details. 9 * 10 * @TAG(DATA61_BSD) 11 */ 12 13/** 14 * Declares macros and methods which are conditional based 15 * on NDEBUG. If NDEBUG is defined then seL4_DebugAssert 16 * is a NOP, otherwise it invokes the unconditional version 17 * in sel4/assert.h. 18 */ 19#ifndef __LIBSEL4_DEBUG_ASSERT_H 20#define __LIBSEL4_DEBUG_ASSERT_H 21 22#ifdef NDEBUG 23 24/** NDEBUG is defined do nothing */ 25#define seL4_DebugAssert(expr) ((void)(0)) 26 27#else // NDEBUG is not defined 28 29#include <sel4/assert.h> 30 31/** 32 * NDEBUG is not defined invoke seL4_Assert(expr). 33 */ 34#define seL4_DebugAssert(expr) seL4_Assert(expr) 35 36#endif // NDEBUG 37 38#endif // __LIBSEL4_DEBUG_ASSERT_H 39