Linux Device Driver Environment: bug.c Source File

00001 /* $Id: bug.c,v 1.2 2003/08/29 10:13:22 ch12 Exp $ */
00002 /*****************************************************************************/
00013 /* (c) 2003 Technische Universitaet Dresden
00014  * This file is part of DROPS, which is distributed under the terms of the
00015  * GNU General Public License 2. Please see the COPYING file for details.
00016  */
00017 
00018 #include <l4/dde_linux/dde.h>
00019 #include <l4/log/l4log.h>
00020 #include <linux/kernel.h>
00021 #include <l4/sys/kdebug.h>
00022 
00023 static void do_bug(const char*, const char*, int) __attribute__ ((noreturn));
00024 
00025 void (*dde_BUG)(const char *file, const char *function, int line) __attribute__ ((noreturn)) = do_bug;
00026 
00027 static void do_bug(const char *file, const char *function, int line)
00028 {
00029   printk("BUG() called in %s:%d(%s)", file, line, function);
00030   LOG_flush();
00031   while (1) enter_kdebug("bug");
00032 }