--- /dev/null
+#include <debug.h>
+#include <stdarg.h>
+#include <stdbool.h>
+#include <stdio.h>
+#include <syscall.h>
+
+/* Aborts the user program, printing the source file name, line
+ number, and function name, plus a user-specific message. */
+void
+debug_panic (const char *file, int line, const char *function,
+ const char *message, ...)
+{
+ va_list args;
+
+ printf ("User process abort at %s:%d in %s(): ", file, line, function);
+
+ va_start (args, message);
+ vprintf (message, args);
+ printf ("\n");
+ va_end (args);
+
+ debug_backtrace ();
+
+ exit (1);
+}