From 5a632954c85e8b2b5afea124e4fc83f39c5d3598 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 1 Jun 2021 14:37:07 +0200 Subject: [BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend/C2C.ml --- common/Builtins0.v | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) (limited to 'common/Builtins0.v') diff --git a/common/Builtins0.v b/common/Builtins0.v index d84c9112..384dde1e 100644 --- a/common/Builtins0.v +++ b/common/Builtins0.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. *) (* *) (* *********************************************************************) @@ -341,6 +342,7 @@ Inductive standard_builtin : Type := | BI_i16_bswap | BI_i32_bswap | BI_i64_bswap + | BI_unreachable | BI_i64_umulh | BI_i64_smulh | BI_i64_sdiv @@ -376,6 +378,7 @@ Definition standard_builtin_table : list (string * standard_builtin) := :: ("__builtin_bswap", BI_i32_bswap) :: ("__builtin_bswap32", BI_i32_bswap) :: ("__builtin_bswap64", BI_i64_bswap) + :: ("__builtin_unreachable", BI_unreachable) :: ("__compcert_i64_umulh", BI_i64_umulh) :: ("__compcert_i64_smulh", BI_i64_smulh) :: ("__compcert_i64_sdiv", BI_i64_sdiv) @@ -414,6 +417,8 @@ Definition standard_builtin_sig (b: standard_builtin) : signature := mksignature (Tlong :: nil) Tlong cc_default | BI_i16_bswap => mksignature (Tint :: nil) Tint cc_default + | BI_unreachable => + mksignature nil Tvoid cc_default | BI_i64_shl | BI_i64_shr | BI_i64_sar => mksignature (Tlong :: Tint :: nil) Tlong cc_default | BI_i64_dtos | BI_i64_dtou => @@ -448,6 +453,7 @@ Program Definition standard_builtin_sem (b: standard_builtin) : builtin_sem (sig | BI_i64_bswap => mkbuiltin_n1t Tlong Tlong (fun n => Int64.repr (decode_int (List.rev (encode_int 8%nat (Int64.unsigned n))))) + | BI_unreachable => mkbuiltin Tvoid (fun vargs => None) _ _ | BI_i64_umulh => mkbuiltin_n2t Tlong Tlong Tlong Int64.mulhu | BI_i64_smulh => mkbuiltin_n2t Tlong Tlong Tlong Int64.mulhs | BI_i64_sdiv => mkbuiltin_v2p Tlong Val.divls _ _ -- cgit