Use # format specifier rather than manually writing 0x for hex numbers.

Change-Id: Ic3f98b33b34ce5ffe3300a5ca9c9c309ef2c056c
diff --git a/src/load.c b/src/load.c
index 78b5777..602cfa8 100644
--- a/src/load.c
+++ b/src/load.c
@@ -347,7 +347,7 @@
 			return false;
 		}
 
-		dlog("Loaded with %u vcpus, entry at 0x%x\n", cpu,
+		dlog("Loaded with %u vcpus, entry at %#x\n", cpu,
 		     pa_addr(secondary_mem_begin));
 
 		vcpu = vm_get_vcpu(vm, 0);