1/*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * This software may be distributed and modified according to the terms of
5 * the GNU General Public License version 2. Note that NO WARRANTY is provided.
6 * See "LICENSE_GPLv2.txt" for details.
7 *
8 * @TAG(GD_GPL)
9 */
10
11#include <assert.h>
12#include <machine/io.h>
13
14#ifdef CONFIG_DEBUG_BUILD
15
16void _fail(
17    const char*  s,
18    const char*  file,
19    unsigned int line,
20    const char*  function)
21{
22    printf(
23        "seL4 called fail at %s:%u in function %s, saying \"%s\"\n",
24        file,
25        line,
26        function,
27        s
28    );
29    halt();
30}
31
32void _assert_fail(
33    const char*  assertion,
34    const char*  file,
35    unsigned int line,
36    const char*  function)
37{
38    printf("seL4 failed assertion '%s' at %s:%u in function %s\n",
39           assertion,
40           file,
41           line,
42           function
43          );
44    halt();
45}
46
47#endif
48