From 09c1f3f549ddccc9326c6d7ec0f928312f4a6295 Mon Sep 17 00:00:00 2001
From: Michael Cardell Widerkrantz <mc@tillitis.se>
Date: Thu, 21 Mar 2024 12:32:08 +0100
Subject: [PATCH] Silence splint somewhat

The only real changes are some unitialized variables and that we now
make explicit that we don't care about the return value from memset().
---
 hw/application_fpga/fw/tk1/assert.c |  2 ++
 hw/application_fpga/fw/tk1/lib.c    |  6 ++++++
 hw/application_fpga/fw/tk1/main.c   | 15 ++++++++++++---
 hw/application_fpga/fw/tk1/proto.c  |  2 +-
 hw/application_fpga/fw/tk1/proto.h  |  1 +
 5 files changed, 22 insertions(+), 4 deletions(-)

diff --git a/hw/application_fpga/fw/tk1/assert.c b/hw/application_fpga/fw/tk1/assert.c
index adce820..2c3d75e 100644
--- a/hw/application_fpga/fw/tk1/assert.c
+++ b/hw/application_fpga/fw/tk1/assert.c
@@ -20,8 +20,10 @@ void assert_fail(const char *assertion, const char *file, unsigned int line,
 	htif_puts(function);
 	htif_lf();
 
+#ifndef S_SPLINT_S
 	// Force illegal instruction to halt CPU
 	asm volatile("unimp");
+#endif
 
 	// Not reached
 	__builtin_unreachable();
diff --git a/hw/application_fpga/fw/tk1/lib.c b/hw/application_fpga/fw/tk1/lib.c
index 8c860eb..ac8b69a 100644
--- a/hw/application_fpga/fw/tk1/lib.c
+++ b/hw/application_fpga/fw/tk1/lib.c
@@ -104,6 +104,7 @@ void *memset(void *dest, int c, unsigned n)
 	for (; n; n--, s++)
 		*s = (uint8_t)c;
 
+	/*@ -temptrans @*/
 	return dest;
 }
 
@@ -117,6 +118,11 @@ void memcpy_s(void *dest, size_t destsize, const void *src, size_t n)
 	uint8_t *dest_byte = (uint8_t *)dest;
 
 	for (size_t i = 0; i < n; i++) {
+		/*@ -nullderef @*/
+		/* splint complains that dest_byte and src_byte can be
+		 * NULL, but it seems it doesn't understand assert.
+		 * See above.
+		 */
 		dest_byte[i] = src_byte[i];
 	}
 }
diff --git a/hw/application_fpga/fw/tk1/main.c b/hw/application_fpga/fw/tk1/main.c
index cce3ca9..8022cff 100644
--- a/hw/application_fpga/fw/tk1/main.c
+++ b/hw/application_fpga/fw/tk1/main.c
@@ -92,8 +92,8 @@ static uint32_t rnd_word(void)
 static void compute_cdi(const uint8_t *digest, const uint8_t use_uss,
 			const uint8_t *uss)
 {
-	uint32_t local_uds[8];
-	uint32_t local_cdi[8];
+	uint32_t local_uds[8] = {0};
+	uint32_t local_cdi[8] = {0};
 	blake2s_ctx secure_ctx = {0};
 	uint32_t rnd_sleep = 0;
 	int blake2err = 0;
@@ -115,7 +115,7 @@ static void compute_cdi(const uint8_t *digest, const uint8_t use_uss,
 	// while on the firmware stack which is in the special fw_ram.
 	wordcpy_s(local_uds, 8, (void *)uds, 8);
 	blake2s_update(&secure_ctx, (const void *)local_uds, 32);
-	memset(local_uds, 0, 32);
+	(void)memset(local_uds, 0, 32);
 
 	// Update with TKey program digest
 	blake2s_update(&secure_ctx, digest, 32);
@@ -268,7 +268,9 @@ static enum state loading_commands(const struct frame_header *hdr,
 			nbytes = ctx->left;
 		}
 		memcpy_s(ctx->loadaddr, ctx->left, cmd + 1, nbytes);
+		/*@-mustfreeonly@*/
 		ctx->loadaddr += nbytes;
+		/*@+mustfreeonly@*/
 		ctx->left -= nbytes;
 
 		if (ctx->left == 0) {
@@ -396,7 +398,12 @@ int main(void)
 	// Let the app know the function adddress for blake2s()
 	*fw_blake2s_addr = (uint32_t)blake2s;
 
+	/*@-mustfreeonly@*/
+	/* Yes, splint, this points directly to RAM and we don't care
+	 * about freeing anything was pointing to 0x0 before.
+	 */
 	ctx.loadaddr = (uint8_t *)TK1_RAM_BASE;
+	/*@+mustfreeonly@*/
 	ctx.use_uss = FALSE;
 
 	scramble_ram();
@@ -436,5 +443,7 @@ int main(void)
 		}
 	}
 
+	/*@ -compdestroy @*/
+	/* We don't care about memory leaks here. */
 	return (int)0xcafebabe;
 }
diff --git a/hw/application_fpga/fw/tk1/proto.c b/hw/application_fpga/fw/tk1/proto.c
index b01a3f7..4acbce4 100644
--- a/hw/application_fpga/fw/tk1/proto.c
+++ b/hw/application_fpga/fw/tk1/proto.c
@@ -167,7 +167,7 @@ static int read(uint8_t *buf, size_t bufsize, size_t nbytes)
 // bytelen returns the number of bytes a cmdlen takes
 static int bytelen(enum cmdlen cmdlen)
 {
-	int len;
+	int len = 0;
 
 	switch (cmdlen) {
 	case LEN_1:
diff --git a/hw/application_fpga/fw/tk1/proto.h b/hw/application_fpga/fw/tk1/proto.h
index 4bf225f..1c13c5c 100644
--- a/hw/application_fpga/fw/tk1/proto.h
+++ b/hw/application_fpga/fw/tk1/proto.h
@@ -50,6 +50,7 @@ struct frame_header {
 	enum cmdlen len;
 };
 
+/*@ -exportlocal @*/
 void writebyte(uint8_t b);
 uint8_t readbyte(void);
 void fwreply(struct frame_header hdr, enum fwcmd rspcode, uint8_t *buf);