Pintos: pintos/src/lib/user/debug.c Source File

00001 #include <debug.h>
00002 #include <stdarg.h>
00003 #include <stdbool.h>
00004 #include <stdio.h>
00005 #include <syscall.h>
00006 
00007 /* Aborts the user program, printing the source file name, line
00008    number, and function name, plus a user-specific message. */
00009 void
00010 debug_panic (const char *file, int line, const char *function,
00011              const char *message, ...)
00012 {
00013   va_list args;
00014 
00015   printf ("User process ABORT at %s:%d in %s(): ", file, line, function);
00016 
00017   va_start (args, message);
00018   vprintf (message, args);
00019   printf ("\n");
00020   va_end (args);
00021 
00022   debug_backtrace ();
00023   
00024   exit (1);
00025 }