From eaed1201750b67c21ec05215b13c80ba381aa968 Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Date: Fri, 3 Oct 2025 09:00:06 +1000
Subject: [PATCH] util: provide FNSPEC for __unreachable

Adding a spec with precondition False means verification has to show
that the function is not called.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
---
 include/util.h | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/include/util.h b/include/util.h
index 891c1210e..12333a1e4 100644
--- a/include/util.h
+++ b/include/util.h
@@ -91,6 +91,9 @@
 #define FORCE_O2     __attribute__((optimize("O2")))
 #endif
 /** MODIFIES: */
+/** FNSPEC
+      StrictC'__unreachable_spec: "\<Gamma> \<turnstile> {} Call StrictC'__unreachable_'proc UNIV"
+ */
 void __builtin_unreachable(void);
 #define UNREACHABLE()  __builtin_unreachable()
 #define MAY_ALIAS    __attribute__((may_alias))