aboutsummaryrefslogtreecommitdiffstats
path: root/arm/Asmexpand.ml
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2021-09-17 18:28:55 +0100
committerYann Herklotz <git@yannherklotz.com>2021-09-17 18:28:55 +0100
commita1c401a4eba5fc9fcf42933f70005ecb679a4c1c (patch)
tree26637fca5d1da9b3d049234721d593a60b03a6d3 /arm/Asmexpand.ml
parentc49caca4b5f0239b43610fbfe012d6ba0211b364 (diff)
parent1daf96cdca4d828c333cea5c9a314ef861342984 (diff)
downloadcompcert-a1c401a4eba5fc9fcf42933f70005ecb679a4c1c.tar.gz
compcert-a1c401a4eba5fc9fcf42933f70005ecb679a4c1c.zip
Merge branch 'master' into dev/michalisdev/michalis
Diffstat (limited to 'arm/Asmexpand.ml')
-rw-r--r--arm/Asmexpand.ml8
1 files changed, 6 insertions, 2 deletions
diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml
index f4e79a37..01b18c37 100644
--- a/arm/Asmexpand.ml
+++ b/arm/Asmexpand.ml
@@ -407,8 +407,12 @@ let expand_builtin_inline name args res =
(* Vararg stuff *)
| "__builtin_va_start", [BA(IR a)], _ ->
expand_builtin_va_start a
+ (* No operation *)
| "__builtin_nop", [], _ ->
emit Pnop
+ (* Optimization hint *)
+ | "__builtin_unreachable", [], _ ->
+ ()
(* Catch-all *)
| _ ->
raise (Error ("unrecognized builtin " ^ name))
@@ -545,7 +549,7 @@ module FixupHF = struct
end
let fixup_arguments dir sg =
- if sg.sig_cc.cc_vararg then
+ if sg.sig_cc.cc_vararg <> None then
FixupEABI.fixup_arguments dir sg
else begin
let act = fixup_actions (Array.make 16 false) 0 sg.sig_args in
@@ -555,7 +559,7 @@ module FixupHF = struct
end
let fixup_result dir sg =
- if sg.sig_cc.cc_vararg then
+ if sg.sig_cc.cc_vararg <> None then
FixupEABI.fixup_result dir sg
end