9 files changed, 11 insertions, 10 deletions
diff --git a/src/arch/x86_64/include/bits/byteswap.h b/src/arch/x86_64/include/bits/byteswap.h
index d8c5098ef..7c48a27ca 100644
--- a/src/arch/x86_64/include/bits/byteswap.h
+++ b/src/arch/x86_64/include/bits/byteswap.h
@@ -10,6 +10,7 @@
 #include <stdint.h>
 
 FILE_LICENCE ( GPL2_OR_LATER_OR_UBDL );
+FILE_SECBOOT ( PERMITTED );
 
 static inline __attribute__ (( always_inline, const )) uint16_t
 __bswap_variable_16 ( uint16_t x ) {
diff --git a/src/arch/x86_64/include/bits/compiler.h b/src/arch/x86_64/include/bits/compiler.h
index 1c04a7b30..99185b058 100644
--- a/src/arch/x86_64/include/bits/compiler.h
+++ b/src/arch/x86_64/include/bits/compiler.h
@@ -2,6 +2,7 @@
 #define _BITS_COMPILER_H
 
 FILE_LICENCE ( GPL2_OR_LATER_OR_UBDL );
+FILE_SECBOOT ( PERMITTED );
 
 /** Dummy relocation type */
 #define RELOC_TYPE_NONE R_X86_64_NONE
diff --git a/src/arch/x86_64/include/gdbmach.h b/src/arch/x86_64/include/bits/gdbmach.h
index 367405fd6..367405fd6 100644
--- a/src/arch/x86_64/include/gdbmach.h
+++ b/src/arch/x86_64/include/bits/gdbmach.h
diff --git a/src/arch/x86_64/include/bits/profile.h b/src/arch/x86_64/include/bits/profile.h
index b7c74fbe7..c8e0a21f1 100644
--- a/src/arch/x86_64/include/bits/profile.h
+++ b/src/arch/x86_64/include/bits/profile.h
@@ -8,6 +8,7 @@
  */
 
 FILE_LICENCE ( GPL2_OR_LATER_OR_UBDL );
+FILE_SECBOOT ( PERMITTED );
 
 #include <stdint.h>
 
@@ -16,7 +17,7 @@ FILE_LICENCE ( GPL2_OR_LATER_OR_UBDL );
  *
  * @ret timestamp	Timestamp
  */
-static inline __attribute__ (( always_inline )) uint64_t
+static inline __attribute__ (( always_inline )) unsigned long
 profile_timestamp ( void ) {
 	uint32_t eax;
 	uint32_t edx;
diff --git a/src/arch/x86_64/include/setjmp.h b/src/arch/x86_64/include/bits/setjmp.h
index 69835d9fa..adfb869ea 100644
--- a/src/arch/x86_64/include/setjmp.h
+++ b/src/arch/x86_64/include/bits/setjmp.h
@@ -1,5 +1,5 @@
-#ifndef _SETJMP_H
-#define _SETJMP_H
+#ifndef _BITS_SETJMP_H
+#define _BITS_SETJMP_H
 
 FILE_LICENCE ( GPL2_OR_LATER_OR_UBDL );
 
@@ -25,10 +25,4 @@ typedef struct {
 	uint64_t r15;
 } jmp_buf[1];
 
-extern int __asmcall __attribute__ (( returns_twice ))
-setjmp ( jmp_buf env );
-
-extern void __asmcall __attribute__ (( noreturn ))
-longjmp ( jmp_buf env, int val );
-
-#endif /* _SETJMP_H */
+#endif /* _BITS_SETJMP_H */
diff --git a/src/arch/x86_64/include/bits/stdint.h b/src/arch/x86_64/include/bits/stdint.h
index fe1f9946a..e75bed502 100644
--- a/src/arch/x86_64/include/bits/stdint.h
+++ b/src/arch/x86_64/include/bits/stdint.h
@@ -2,6 +2,7 @@
 #define _BITS_STDINT_H
 
 FILE_LICENCE ( GPL2_OR_LATER_OR_UBDL );
+FILE_SECBOOT ( PERMITTED );
 
 typedef __SIZE_TYPE__		size_t;
 typedef signed long		ssize_t;
diff --git a/src/arch/x86_64/include/bits/strings.h b/src/arch/x86_64/include/bits/strings.h
index 3b7911f3b..6da8f1350 100644
--- a/src/arch/x86_64/include/bits/strings.h
+++ b/src/arch/x86_64/include/bits/strings.h
@@ -2,6 +2,7 @@
 #define _BITS_STRINGS_H
 
 FILE_LICENCE ( GPL2_OR_LATER_OR_UBDL );
+FILE_SECBOOT ( PERMITTED );
 
 /**
  * Find first (i.e. least significant) set bit
diff --git a/src/arch/x86_64/include/ipxe/efi/dhcparch.h b/src/arch/x86_64/include/ipxe/efi/dhcparch.h
index ccf0f46a0..f75bf9145 100644
--- a/src/arch/x86_64/include/ipxe/efi/dhcparch.h
+++ b/src/arch/x86_64/include/ipxe/efi/dhcparch.h
@@ -8,6 +8,7 @@
  */
 
 FILE_LICENCE ( GPL2_OR_LATER_OR_UBDL );
+FILE_SECBOOT ( PERMITTED );
 
 #include <ipxe/dhcp.h>
 
diff --git a/src/arch/x86_64/include/limits.h b/src/arch/x86_64/include/limits.h
index a1374a17f..e75461acb 100644
--- a/src/arch/x86_64/include/limits.h
+++ b/src/arch/x86_64/include/limits.h
@@ -2,6 +2,7 @@
 #define LIMITS_H	1
 
 FILE_LICENCE ( GPL2_OR_LATER_OR_UBDL );
+FILE_SECBOOT ( PERMITTED );
 
 /* Number of bits in a `char' */
 #define CHAR_BIT	8