commit fcbc1944a948c651cabaa509c55dc0dcdf3ed377
author Axel Heider <axelheider@gmx.de> Mon Mar 15 06:28:58 2021 +0100
committer Kent McLeod <kent-mcleod@users.noreply.github.com> Thu Mar 25 16:51:15 2021 +1100
tree 26ce84de5d4a8c4c9033be0f2b47040e8eb25387
parent d5b36675f890eeda58a3bb2b8d158dc683dcc803

fail cap checks if CONFIG_DEBUG_BUILD is not set

Signed-off-by: Axel Heider <axelheider@gmx.de>

libsel4debug/include/sel4debug/debug.h

diff --git a/libsel4debug/include/sel4debug/debug.h b/libsel4debug/include/sel4debug/debug.h
index ad0f2bc..1e327f7 100644
--- a/libsel4debug/include/sel4debug/debug.h
+++ b/libsel4debug/include/sel4debug/debug.h
@@ -24,21 +24,33 @@
 #ifdef CONFIG_DEBUG_BUILD
 static inline int debug_cap_is_valid(seL4_CPtr cap)
 {
+#ifdef CONFIG_DEBUG_BUILD
     return (0 != seL4_DebugCapIdentify(cap));
+#else
+    return 0; /* fail check on non-debug kernels */
+#endif
 }
 
 static inline int debug_cap_is_endpoint(seL4_CPtr cap)
 {
+#ifdef CONFIG_DEBUG_BUILD
     // there is kernel/generated/arch/object/structures_gen.h that defines
     // cap_endpoint_cap = 4, but we can't include it here
     return (4 == seL4_DebugCapIdentify(cap));
+#else
+    return 0; /* fail check on non-debug kernels */
+#endif
 }
 
 static inline int debug_cap_is_notification(seL4_CPtr cap)
 {
+#ifdef CONFIG_DEBUG_BUILD
     // there is kernel/generated/arch/object/structures_gen.h that defines
     // cap_notification_cap = 6, but we can't include it here
     return (6 == seL4_DebugCapIdentify(cap));
+#else
+    return 0; /* fail check on non-debug kernels */
+#endif
 }
 #endif /* CONFIG_DEBUG_BUILD */
 

libsel4debug/src/caps.c

diff --git a/libsel4debug/src/caps.c b/libsel4debug/src/caps.c
index e9ba4c2..c29b304 100644
--- a/libsel4debug/src/caps.c
+++ b/libsel4debug/src/caps.c
@@ -14,7 +14,8 @@
 {
 #ifdef CONFIG_DEBUG_BUILD
     int type = seL4_DebugCapIdentify(cap);
-
-    printf("Cap type number is %d\n", type);
-#endif /* CONFIG_DEBUG_BUILD */
+    printf("Cap %d has type %d\n", cap, type);
+#else
+    printf("DEBUG_BUILD not set, can't get type of cap %d", cap);
+#endif
 }