Index: kernel/generic/src/debug/util.h
===================================================================
--- kernel/generic/src/debug/util.h	(revision 001957b64a7ead0eaa50ef46f3832f77e1902798)
+++ kernel/generic/src/debug/util.h	(revision b1397ab53bc6bd57626e42c92953b27cad139528)
@@ -33,4 +33,5 @@
 #include <stdint.h>
 #include <debug/constants.h>
+#include <debug/sections.h>
 #include <debug.h>
 
@@ -39,11 +40,11 @@
 extern bool skip_data(unsigned, const uint8_t **const, const uint8_t *, unsigned);
 extern void print_format(const char *, const uint8_t *, const uint8_t *);
-extern void print_formatted_list(const char *, const uint8_t *, const uint8_t *,
-    const uint8_t *, const uint8_t *, unsigned);
+extern void print_formatted_list(debug_sections_t *, const char *,
+    const uint8_t *, const uint8_t *, const uint8_t *, const uint8_t *, unsigned);
 
 extern void print_block(const uint8_t **, const uint8_t *, unsigned);
-extern void print_formed_data(unsigned, const uint8_t **const, const uint8_t *, unsigned);
-
-inline uint8_t read_byte(const uint8_t **data, const uint8_t *data_end)
+extern void print_formed_data(debug_sections_t *scs, unsigned, const uint8_t **const, const uint8_t *, unsigned);
+
+static inline uint8_t read_byte(const uint8_t **data, const uint8_t *data_end)
 {
 	if (*data >= data_end) {
@@ -67,5 +68,5 @@
 } __attribute__((packed));
 
-inline uint16_t read_uint16(const uint8_t **data, const uint8_t *data_end)
+static inline uint16_t read_uint16(const uint8_t **data, const uint8_t *data_end)
 {
 	if (*data + 2 > data_end) {
@@ -80,5 +81,5 @@
 }
 
-inline uint32_t read_uint24(const uint8_t **data, const uint8_t *data_end)
+static inline uint32_t read_uint24(const uint8_t **data, const uint8_t *data_end)
 {
 	if (*data + 3 > data_end) {
@@ -98,5 +99,5 @@
 }
 
-inline uint32_t read_uint32(const uint8_t **data, const uint8_t *data_end)
+static inline uint32_t read_uint32(const uint8_t **data, const uint8_t *data_end)
 {
 	if (*data + 4 > data_end) {
@@ -111,5 +112,5 @@
 }
 
-inline uint64_t read_uint64(const uint8_t **data, const uint8_t *data_end)
+static inline uint64_t read_uint64(const uint8_t **data, const uint8_t *data_end)
 {
 	if (*data + 8 > data_end) {
@@ -124,5 +125,5 @@
 }
 
-inline uint64_t read_uint(const uint8_t **data, const uint8_t *data_end, unsigned bytes)
+static inline uint64_t read_uint(const uint8_t **data, const uint8_t *data_end, unsigned bytes)
 {
 	switch (bytes) {
@@ -140,5 +141,5 @@
 }
 
-inline uint64_t read_uleb128(const uint8_t **data, const uint8_t *data_end)
+static inline uint64_t read_uleb128(const uint8_t **data, const uint8_t *data_end)
 {
 	uint64_t result = 0;
@@ -157,5 +158,5 @@
 }
 
-inline int64_t read_sleb128(const uint8_t **data, const uint8_t *data_end)
+static inline int64_t read_sleb128(const uint8_t **data, const uint8_t *data_end)
 {
 	uint64_t result = 0;
@@ -179,5 +180,5 @@
 }
 
-inline void skip_leb128(const uint8_t **data, const uint8_t *data_end)
+static inline void skip_leb128(const uint8_t **data, const uint8_t *data_end)
 {
 	while (*data < data_end) {
@@ -188,5 +189,5 @@
 }
 
-inline uint64_t read_initial_length(const uint8_t **data, const uint8_t *data_end, unsigned *width)
+static inline uint64_t read_initial_length(const uint8_t **data, const uint8_t *data_end, unsigned *width)
 {
 	uint32_t initial = read_uint32(data, data_end);
@@ -200,5 +201,5 @@
 }
 
-inline const char *read_string(const uint8_t **data, const uint8_t *data_end)
+static inline const char *read_string(const uint8_t **data, const uint8_t *data_end)
 {
 	const char *start = (const char *) *data;
@@ -218,10 +219,10 @@
 }
 
-inline void skip_string(const uint8_t **data, const uint8_t *data_end)
+static inline void skip_string(const uint8_t **data, const uint8_t *data_end)
 {
 	(void) read_string(data, data_end);
 }
 
-inline void safe_increment(const uint8_t **data,
+static inline void safe_increment(const uint8_t **data,
     const uint8_t *data_end, ptrdiff_t increment)
 {
@@ -235,5 +236,5 @@
 }
 
-inline void skip_format(const uint8_t **data, const uint8_t *const data_end,
+static inline void skip_format(const uint8_t **data, const uint8_t *const data_end,
     unsigned count)
 {
@@ -244,5 +245,5 @@
 }
 
-inline void skip_formatted_entry(const uint8_t **data, const uint8_t *const data_end,
+static inline void skip_formatted_entry(const uint8_t **data, const uint8_t *const data_end,
     const uint8_t *format, const uint8_t *format_end, unsigned width)
 {
@@ -256,5 +257,5 @@
 }
 
-inline void skip_formatted_list(const uint8_t **data, const uint8_t *const data_end,
+static inline void skip_formatted_list(const uint8_t **data, const uint8_t *const data_end,
     unsigned count,	const uint8_t *format, const uint8_t *format_end,
     unsigned width)
