aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@college-de-france.fr>2021-04-25 13:57:47 +0200
committerXavier Leroy <xavierleroy@users.noreply.github.com>2021-05-02 18:06:32 +0200
commit320c55590cc30d4ef5b2c1a226f0f940a6bdb445 (patch)
treeed6ad57e251e164fec31c57a6f2162daabc8305d /aarch64
parent38b0babd5a642cea8912524debc63edc67fda08b (diff)
downloadcompcert-kvx-320c55590cc30d4ef5b2c1a226f0f940a6bdb445.tar.gz
compcert-kvx-320c55590cc30d4ef5b2c1a226f0f940a6bdb445.zip
Support __builtin_unreachable
Not yet used for optimizations.
Diffstat (limited to 'aarch64')
-rw-r--r--aarch64/Asmexpand.ml4
1 files changed, 4 insertions, 0 deletions
diff --git a/aarch64/Asmexpand.ml b/aarch64/Asmexpand.ml
index 6c80e9d3..d24a9ef6 100644
--- a/aarch64/Asmexpand.ml
+++ b/aarch64/Asmexpand.ml
@@ -355,8 +355,12 @@ let expand_builtin_inline name args res =
(* Synchronization *)
| "__builtin_membar", [], _ ->
()
+ (* No operation *)
| "__builtin_nop", [], _ ->
emit Pnop
+ (* Optimization hint *)
+ | "__builtin_unreachable", [], _ ->
+ ()
(* Byte swap *)
| ("__builtin_bswap" | "__builtin_bswap32"), [BA(IR a1)], BR(IR res) ->
emit (Prev(W, res, a1))