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