aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64
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 /aarch64
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 'aarch64')
-rw-r--r--aarch64/Archi.v9
-rw-r--r--aarch64/Asmexpand.ml4
-rw-r--r--aarch64/Builtins1.v9
-rw-r--r--aarch64/CBuiltins.ml9
-rw-r--r--aarch64/extractionMachdep.v9
5 files changed, 24 insertions, 16 deletions
diff --git a/aarch64/Archi.v b/aarch64/Archi.v
index b47ce91f..378ca0d1 100644
--- a/aarch64/Archi.v
+++ b/aarch64/Archi.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/aarch64/Asmexpand.ml b/aarch64/Asmexpand.ml
index 6863b967..828c96d6 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(DR(IR(RR1 a1)))], BR(DR(IR(RR1 res))) ->
emit (Prev(W, res, a1))
diff --git a/aarch64/Builtins1.v b/aarch64/Builtins1.v
index 53c83d7e..cd6f8cc4 100644
--- a/aarch64/Builtins1.v
+++ b/aarch64/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/aarch64/CBuiltins.ml b/aarch64/CBuiltins.ml
index 4cfb7edf..80d66310 100644
--- a/aarch64/CBuiltins.ml
+++ b/aarch64/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/aarch64/extractionMachdep.v b/aarch64/extractionMachdep.v
index dc117744..0401d0fa 100644
--- a/aarch64/extractionMachdep.v
+++ b/aarch64/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. *)
(* *)
(* *********************************************************************)