diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 1753414b85b25a9e1a7bcbe0fb05360a7dce6e97..31f23651a1d6aa54ddea88e1bac02e81fcf2c883 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -6296,7 +6296,41 @@ and doExp local_env
             (new_exp ~loc (Lval (var tmp)))
             intType
       end
-
+    | Cabs.CALL({ expr_node = VARIABLE "__builtin_choose_expr"},
+                args, ghost_args)
+        when Cil.gccMode() ->
+        (* __builtin_choose_expr is supposed to choose at compile time between
+           two expressions, hence we have to handle it separately from the
+           normal calls. *)
+        begin
+          match args, ghost_args with
+          | [ cond; e1; e2 ], [] ->
+            let _, chunk, cond, _ =
+              doExp (no_paren_local_env local_env) CConst cond (AExp None)
+            in
+            if not (isEmpty chunk) then
+              abort_context ~loc:cond.eloc
+                "first argument of __builtin_choose_expr \
+                 shouldn't have side effect";
+            let cond_is_true =
+              match (Cil.constFold true cond).enode with
+              | Const (CInt64 (v,_,_)) -> not (Z.equal v Z.zero)
+              | Const (CReal(v,_,_)) -> Fc_float.compare v 0. <> 0
+              | Const (CChr c) -> Char.code c <> 0
+              | Const (CStr _) | Const (CWStr _) -> true
+              | _ ->
+                abort_context ~loc:cond.eloc
+                  "first argument of __builtin_choose_expr should be \
+                   a compile-time constant"
+            in
+            if cond_is_true then begin
+              doExp (no_paren_local_env local_env) asconst e1 what
+            end else begin
+              doExp (no_paren_local_env local_env) asconst e2 what
+            end
+          | _ ->
+            abort_context "ill-formed call to __builtin_choose_expr"
+        end
     | Cabs.CALL(f, args, ghost_args) ->
       let (rf,sf, f', ft') =
         match (stripParen f).expr_node with
diff --git a/tests/syntax/builtin_choose_expr.i b/tests/syntax/builtin_choose_expr.i
new file mode 100644
index 0000000000000000000000000000000000000000..c1205b1fef5ec608436bcf526af4d88dce9f1ec4
--- /dev/null
+++ b/tests/syntax/builtin_choose_expr.i
@@ -0,0 +1,8 @@
+/* run.config
+   OPT: -machdep gcc_x86_64 -print
+*/
+int f() {
+  int x = __builtin_choose_expr(sizeof(char) == 1, 42, 3.f);
+  float y = __builtin_choose_expr(sizeof(char) == 1, 3.f, 42);
+  return x;
+}
diff --git a/tests/syntax/oracle/builtin_choose_expr.res.oracle b/tests/syntax/oracle/builtin_choose_expr.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..7f70352fd4ebe7db2ff7871f2e6cc12f7915725f
--- /dev/null
+++ b/tests/syntax/oracle/builtin_choose_expr.res.oracle
@@ -0,0 +1,10 @@
+[kernel] Parsing builtin_choose_expr.i (no preprocessing)
+/* Generated by Frama-C */
+int f(void)
+{
+  int x = 42;
+  float y = 3.f;
+  return x;
+}
+
+