From 320c55590cc30d4ef5b2c1a226f0f940a6bdb445 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Sun, 25 Apr 2021 13:57:47 +0200
Subject: Support __builtin_unreachable

Not yet used for optimizations.
---
 cfrontend/C2C.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'cfrontend')

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index fee3d86e..8b205d19 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -268,6 +268,9 @@ let builtins_generic = {
         (TPtr(TVoid [], []),
           [TPtr(TVoid [], []); TInt(IULong, [])],
           false);
+  (* Optimization hints *)
+    "__builtin_unreachable",
+        (TVoid [], [], false);
   (* Helper functions for int64 arithmetic *)
     "__compcert_i64_dtos",
         (TInt(ILongLong, []),
-- 
cgit