From b892d177945e9a5188cebe58f277a9d62dc6675e Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Thu, 16 Sep 2021 13:48:43 +0200
Subject: reachable

---
 kvx/Asmblockgen.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kvx/Asmblockgen.v')

diff --git a/kvx/Asmblockgen.v b/kvx/Asmblockgen.v
index e218f4ef..ab827b1c 100644
--- a/kvx/Asmblockgen.v
+++ b/kvx/Asmblockgen.v
@@ -299,7 +299,7 @@ Definition btest_for_cmpuwz (c: comparison) :=
   match c with
   | Cne => OK BTwnez
   | Ceq => OK BTweqz
-  | Clt => Error (msg "btest_for_compuwz: Clt")
+  | Clt => Error (msg "btest_for_compuwz: Clt") (* TODO reachable *)
   | Cge => Error (msg "btest_for_compuwz: Cge")
   | Cle => OK BTweqz
   | Cgt => OK BTwnez
-- 
cgit