#include <stdarg.h>
#include <sys/syscall.h>

int vsprintf(char *buf, const char *fmt, va_list args);

/* Send message to Kernel Output */
void
dbgprintf(char *fmt, ...)
{
	char buf[1024];
	va_list args;
	va_start(args, fmt);
	vsprintf(buf, fmt, args);
	va_end(args);

	int ret;
	char *p = buf;
	asm volatile("int $0x80" : "=a" (ret) : "0" (SYSCALL_DBGPRINTF),
	             "c" (1), "S" (&p));
}

/* Send an unformatted message to Kernel Output */
void
dbgputs(char *str)
{
	int ret;
	asm volatile("int $0x80" : "=a" (ret) : "0" (SYSCALL_DBGPRINTF),
	             "c" (1), "S" (&str));

}