aboutsummaryrefslogtreecommitdiffstats
path: root/x86
diff options
context:
space:
mode:
authorCyril SIX <cyril.six@kalray.eu>2021-06-01 14:37:07 +0200
committerCyril SIX <cyril.six@kalray.eu>2021-06-01 14:37:07 +0200
commit5a632954c85e8b2b5afea124e4fc83f39c5d3598 (patch)
treed53323083adec47d3338a04b516265c634806bea /x86
parenta298e55fdc51cce92a8b39280643b623d7d991a8 (diff)
downloadcompcert-kvx-5a632954c85e8b2b5afea124e4fc83f39c5d3598.tar.gz
compcert-kvx-5a632954c85e8b2b5afea124e4fc83f39c5d3598.zip
[BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend/C2C.ml
Diffstat (limited to 'x86')
-rw-r--r--x86/Asmexpand.ml5
-rw-r--r--x86/Builtins1.v9
-rw-r--r--x86/CBuiltins.ml9
-rw-r--r--x86/extractionMachdep.v9
4 files changed, 19 insertions, 13 deletions
diff --git a/x86/Asmexpand.ml b/x86/Asmexpand.ml
index ecdf97f7..e2c556c7 100644
--- a/x86/Asmexpand.ml
+++ b/x86/Asmexpand.ml
@@ -487,9 +487,12 @@ let expand_builtin_inline name args res =
(* Synchronization *)
| "__builtin_membar", [], _ ->
()
- (* no operation *)
+ (* No operation *)
| "__builtin_nop", [], _ ->
emit Pnop
+ (* Optimization hint *)
+ | "__builtin_unreachable", [], _ ->
+ ()
(* Catch-all *)
| _ ->
raise (Error ("unrecognized builtin " ^ name))
diff --git a/x86/Builtins1.v b/x86/Builtins1.v
index f1d60961..e5233ff5 100644
--- a/x86/Builtins1.v
+++ b/x86/Builtins1.v
@@ -6,10 +6,11 @@
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
-(* under the terms of the GNU General Public License as published by *)
-(* the Free Software Foundation, either version 2 of the License, or *)
-(* (at your option) any later version. This file is also distributed *)
-(* under the terms of the INRIA Non-Commercial License Agreement. *)
+(* under the terms of the GNU Lesser General Public License as *)
+(* published by the Free Software Foundation, either version 2.1 of *)
+(* the License, or (at your option) any later version. *)
+(* This file is also distributed under the terms of the *)
+(* INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
diff --git a/x86/CBuiltins.ml b/x86/CBuiltins.ml
index a16f3ef7..a549cd25 100644
--- a/x86/CBuiltins.ml
+++ b/x86/CBuiltins.ml
@@ -6,10 +6,11 @@
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
-(* under the terms of the GNU General Public License as published by *)
-(* the Free Software Foundation, either version 2 of the License, or *)
-(* (at your option) any later version. This file is also distributed *)
-(* under the terms of the INRIA Non-Commercial License Agreement. *)
+(* under the terms of the GNU Lesser General Public License as *)
+(* published by the Free Software Foundation, either version 2.1 of *)
+(* the License, or (at your option) any later version. *)
+(* This file is also distributed under the terms of the *)
+(* INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
diff --git a/x86/extractionMachdep.v b/x86/extractionMachdep.v
index 614ec589..26a3f0a7 100644
--- a/x86/extractionMachdep.v
+++ b/x86/extractionMachdep.v
@@ -6,10 +6,11 @@
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
-(* under the terms of the GNU General Public License as published by *)
-(* the Free Software Foundation, either version 2 of the License, or *)
-(* (at your option) any later version. This file is also distributed *)
-(* under the terms of the INRIA Non-Commercial License Agreement. *)
+(* under the terms of the GNU Lesser General Public License as *)
+(* published by the Free Software Foundation, either version 2.1 of *)
+(* the License, or (at your option) any later version. *)
+(* This file is also distributed under the terms of the *)
+(* INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)