Index: sys/ddb/db_output.c
===================================================================
--- sys/ddb/db_output.c
+++ sys/ddb/db_output.c
@@ -316,13 +316,12 @@
  * Printing
  */
 int
-db_printf(const char *fmt, ...)
+db_vprintf(const char *fmt, va_list listp)
 {
 #ifdef DDB_BUFR_SIZE
 	char bufr[DDB_BUFR_SIZE];
 #endif
 	struct dbputchar_arg dca;
-	va_list	listp;
 	int retval;
 
 #ifdef DDB_BUFR_SIZE
@@ -335,9 +334,7 @@
 	dca.da_pbufr = NULL;
 #endif
 
-	va_start(listp, fmt);
 	retval = kvprintf (fmt, db_putchar, &dca, db_radix, listp);
-	va_end(listp);
 
 #ifdef DDB_BUFR_SIZE
 	if (*dca.da_pbufr != '\0')
@@ -346,6 +343,19 @@
 	return (retval);
 }
 
+int
+db_printf(const char *fmt, ...)
+{
+	va_list	listp;
+	int retval;
+
+	va_start(listp, fmt);
+	retval = db_vprintf(fmt, listp);
+	va_end(listp);
+
+	return (retval);
+}
+
 int db_indent;
 
 void
Index: sys/ddb/ddb.h
===================================================================
--- sys/ddb/ddb.h
+++ sys/ddb/ddb.h
@@ -209,6 +209,7 @@
 void		db_print_loc_and_inst(db_addr_t loc);
 void		db_print_thread(void);
 int		db_printf(const char *fmt, ...) __printflike(1, 2);
+int		db_vprintf(const char *fmt, __va_list) __printflike(1, 0);
 int		db_read_bytes(vm_offset_t addr, size_t size, char *data);
 				/* machine-dependent */
 int		db_readline(char *lstart, int lsize);