debug.c

Go to the documentation of this file.

#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);
}