aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/C2C.ml
diff options
context:
space:
mode:
Diffstat (limited to 'cfrontend/C2C.ml')
-rw-r--r--cfrontend/C2C.ml17
1 files changed, 13 insertions, 4 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 61172dda..22c9466b 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.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. *)
(* *)
(* *********************************************************************)
@@ -282,6 +283,11 @@ let builtins_generic = {
(TPtr(TVoid [], []),
[TPtr(TVoid [], []); TInt(IULong, [])],
false);
+ (* Optimization hints *)
+ "__builtin_unreachable",
+ (TVoid [], [], false);
+ "__builtin_expect",
+ (TInt(ILong, []), [TInt(ILong, []); TInt(ILong, [])], false);
(* Helper functions for int64 arithmetic *)
"__compcert_i64_dtos",
(TInt(ILongLong, []),
@@ -1035,6 +1041,9 @@ let rec convertExpr env e =
ewrap (Ctyping.eselection (convertExpr env arg1)
(convertExpr env arg2) (convertExpr env arg3))
+ | C.ECall({edesc = C.EVar {name = "__builtin_expect"}}, [arg1; arg2]) ->
+ convertExpr env arg1
+
| C.ECall({edesc = C.EVar {name = "printf"}}, args)
when !Clflags.option_interp ->
let targs = convertTypArgs env [] args