From 47b166f7b4e474cd48088f3cdfb897f39af3ce09 Mon Sep 17 00:00:00 2001 From: Virgile Prevosto <virgile.prevosto@cea.fr> Date: Thu, 29 Aug 2024 16:25:09 +0200 Subject: [PATCH] [kernel] post-rebase fix (deprecated fun) --- src/kernel_internals/typing/cabs2cil.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index b7aead68ca..15077459b6 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -6298,7 +6298,7 @@ and doExp local_env end | Cabs.CALL({ expr_node = VARIABLE "__builtin_choose_expr"}, args, ghost_args) - when Cil.gccMode() -> + when Machine.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. *) -- GitLab