aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend
diff options
context:
space:
mode:
Diffstat (limited to 'cfrontend')
-rw-r--r--cfrontend/C2C.ml5
1 files changed, 3 insertions, 2 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index dc25b516..421c4b07 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -157,9 +157,10 @@ let ais_annot_functions =
let builtins_generic = {
builtin_typedefs = [];
builtin_functions =
- ais_annot_functions
- @
+ ais_annot_functions @
[
+ "__builtin_expect",
+ (TInt(ILong, []), [TInt(ILong, []); TInt(ILong, [])], false);
(* Integer arithmetic *)
"__builtin_bswap64",
(TInt(IULongLong, []), [TInt(IULongLong, [])], false);