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 for sel4 specific assert and fail. 15 * 16 * These are unconditional, there are conditional versions of 17 * these in debug_assert.h and are name seL4_DebugAssert and 18 * sl4_DebugCompileTimeAsssert. 19 */ 20 21#ifndef __LIBSEL4_ASSERT_H 22#define __LIBSEL4_ASSERT_H 23 24/** 25 * Hidden function, use the macros seL4_Fail or seL4_Assert. 26 */ 27void __assert_fail(const char* str, const char* file, int line, const char* function); 28 29/** 30 * If expr evaluates to false _seL4_Fail is called with the 31 * expr as a string plus the file, line and function. 32 */ 33#define seL4_Fail(s) __assert_fail(s, __FILE__, __LINE__, __func__) 34 35/** 36 * If expr evaluates to false _seL4_AssertFail is called with the 37 * expr as a string plus the file, line and function. 38 */ 39#define seL4_Assert(expr) \ 40 do { if (!(expr)) { __assert_fail(#expr, __FILE__, __LINE__, __FUNCTION__); } } while(0) 41 42/** 43 * An assert that tests that the expr is a compile time constant and 44 * evaluates to true. 45 * 46 * This code is similar to compile_time_assert in libutils/include/utils/compile_time.h, 47 * we may want to have only one. Also, using __COUNTER__ its not necessary to have name 48 * for uniqueness so I've removed it, although maybe there is another reason for it, like 49 * some compilers don't support __COUNTER__. 50 */ 51#define seL4_CompileTimeAssert(expr) \ 52 extern char __seL4_CompileTimeAssertFailed_ ## __COUNTER__[__builtin_constant_p(expr) ? ((expr) ? 1 : -1) : -1] __attribute__((unused)) 53 54#endif // __LIBSEL4_ASSERT_H 55