diff --git a/doc/userman/user-changes.tex b/doc/userman/user-changes.tex
index b2868d04b708fb8cd4ad4436f4ac9390f64af6f2..b3a1cd537adee172e63ca1277749817319e304be 100644
--- a/doc/userman/user-changes.tex
+++ b/doc/userman/user-changes.tex
@@ -3,7 +3,13 @@
 This chapter summarizes the changes in this documentation between each \FramaC
 release. First we list changes of the last release.
 
-%\section*{Frama-C+dev}
+\section*{Frama-C+dev}
+\begin{itemize}
+\item \textbf{Normalizing the Source Code:} extend and replace options
+  \texttt{-keep-unused-specified-functions} and
+  \texttt{-remove-unused-specified-functions} with
+  \texttt{-keep-unused-functions}.
+\end{itemize}
 
 \section*{29.0 (Copper)}
 \begin{itemize}
diff --git a/doc/userman/user-sources.tex b/doc/userman/user-sources.tex
index 2fb46c266137876d0d077ddf8f48286aba43cfee..6b6fbb73637d63a1e75f5bda809a874ed62aac91 100644
--- a/doc/userman/user-sources.tex
+++ b/doc/userman/user-sources.tex
@@ -258,10 +258,16 @@ a negative value, and choose the smallest rank possible starting from
   Other plug-ins may prefer this option to be used because it better
   preserves the structure of the original program.
 
-\item \optiondef{-}{keep-unused-specified-functions} does not remove from the
-  AST uncalled function prototypes that have ACSL contracts. This option is
-  set by default. So you mostly use the opposite form, namely
-  \optiondef{-}{remove-unused-specified-functions}.
+\item \texttt{\optiondef{-}{keep-unused-functions} <value>} defines which
+  unused function prototypes are kept in the AST. By default (value
+  \texttt{specified}), only those with ACSL specifications are preserved;
+  the user can force those to be removed as well (with value \texttt{none}),
+  or keep prototypes that are both unused and unspecified (value \texttt{all}).
+  A special value \texttt{all\_debug} also preserves predefined prototypes
+  (e.g. compiler builtins).
+  This option extends and replaces previous options
+  \texttt{-keep-unused-specified-functions} and
+  \texttt{-remove-unused-specified-functions}.
 
 \item \optiondef{-}{keep-unused-types} does not remove unused types and
   enum/struct/union declarations. By default, such types are removed,
diff --git a/man/frama-c.1 b/man/frama-c.1
index d73aecf02e488b60f421d871cca4c9b868ec905b..af751133d7619229d9fe423b3b9f034859f5f1c7 100644
--- a/man/frama-c.1
+++ b/man/frama-c.1
@@ -1,7 +1,6 @@
-.\" Automatically generated by Pandoc 2.14.0.3
+.\" Automatically generated by Pandoc 3.1.8
 .\"
 .TH "FRAMA-C" "1" "" "2024-04-24" ""
-.hy
 .\"------------------------------------------------------------------------
 .\"                                                                        
 .\"  This file is part of Frama-C documentation                            
@@ -18,15 +17,12 @@
 .\" using pandoc 2.0 or newer. To modify this file, edit the Markdown file,
 .\" run `dune build @check-man` and then `dune promote`.
 .SH NAME
-.PP
 frama-c - a static analyzer for C programs
 .PP
 frama-c-gui - the graphical interface of frama-c
 .SH SYNOPSIS
-.PP
 \f[B]frama-c\f[R] [ \f[I]options\f[R] ] \f[I]files\f[R]
 .SH DESCRIPTION
-.PP
 \f[B]frama-c\f[R] is a suite of tools dedicated to the analysis of
 source code written in C.
 It gathers several analysis techniques in a single collaborative
@@ -57,7 +53,6 @@ Preprocessing can be customized through the \f[B]-cpp-command\f[R] and
 \f[B]-cpp-extra-args\f[R] options.
 .SH OPTIONS
 .SS Syntax
-.PP
 Options taking an additional parameter can also be written under the
 form
 .RS
@@ -179,8 +174,8 @@ version of this option) when a typechecking error occurs is to reject
 the source file as is the case for typechecking errors within the C
 code.
 With this option on, the typechecker will only output a warning and
-discard the annotation but type\[hy]checking will continue (errors in C
-code are still fatal, though).
+discard the annotation but type‐checking will continue (errors in C code
+are still fatal, though).
 .PD 0
 .P
 .PD
@@ -209,8 +204,7 @@ Note that this option is often better replaced by
 .TP
 -cpp-extra-args \f[I]args\f[R]
 gives additional arguments to the preprocessor.
-Preprocessing annotations is done in two separate preprocessing
-stages.
+Preprocessing annotations is done in two separate preprocessing stages.
 The first one is a normal pass on the C code which retains macro
 definitions.
 These are then used in the second pass during which annotations are
@@ -308,8 +302,14 @@ Defaults to no.
 when \f[B]-simplify-cfg\f[R] is set, keeps switch statements.
 Defaults to no.
 .TP
--keep-unused-specified-functions
-see \f[B]-remove-unused-specified-functions\f[R].
+-keep-unused-functions \f[I]criterion\f[R]
+keeps or removes function prototypes for functions that have no body and
+are not used.
+\f[I]criterion\f[R] is one of: \f[B]none\f[R], \f[B]specified\f[R],
+\f[B]all\f[R], and \f[B]all_debug\f[R]; \f[B]specified\f[R] (the default
+value) keeps function prototypes that have an ACSL specification.
+\f[B]all\f[R] and \f[B]all_debug\f[R] are identical except for compiler
+builtins, which are only included with \f[B]all_debug\f[R].
 .TP
 -keep-unused-types
 see \f[B]-remove-unused-types\f[R].
@@ -456,12 +456,6 @@ inlined.
 removes the given projects \f[I]p1,\&...,pn\f[R].
 \f[B]\[at]all_but_current\f[R] removes all projects but the current one.
 .TP
--remove-unused-specified-functions
-keeps function prototypes that have an ACSL specification but are not
-used in the code.
-This is the default.
-Functions having the attribute \f[B]FRAMAC_BUILTIN\f[R] are always kept.
-.TP
 -remove-unused-types
 remove types and struct/union/enum declarations that are not referenced
 anywhere else in the code.
@@ -491,7 +485,8 @@ statements before analyses.
 Defaults to no.
 .TP
 [-no]-simplify-trivial-loops
-simplifies trivial loops such as \f[B]do \&... while (0)\f[R] loops.
+simplifies trivial loops such as \f[B]do \&...
+while (0)\f[R] loops.
 Defaults to yes.
 .TP
 -then
@@ -526,12 +521,13 @@ syntactically unroll loops \f[I]n\f[R] times before the analysis.
 This can be quite costly and some plugins (e.g.\ Eva) provide more
 efficient ways to perform the same thing.
 See their respective manuals for more information.
-This can also be activated on a per-loop basis via the \f[B]loop pragma
-unroll \f[R] directive.
+This can also be activated on a per-loop basis via the \f[B]loop unfold
+\f[R] directive.
 A negative value for \f[I]n\f[R] will inhibit such pragmas.
 .TP
 [-no]-ulevel-force
-ignores \f[B]UNROLL\f[R] loop pragmas disabling unrolling.
+ignores \f[B]loop unfold \[lq]done\[rq]\f[R] disabling syntactic loop
+unrolling.
 .PP
 [-no]-unicode outputs ACSL formulas with UTF-8 characters.
 This is the default.
@@ -601,7 +597,6 @@ Defaults to no.
 generates alarms for reads of trap representations of _Bool lvalues.
 Defaults to yes.
 .SS Plugin-specific options
-.PP
 For each plugin, the command
 .RS
 .PP
@@ -633,7 +628,6 @@ Exit statuses greater than 2 can be considered as a bug (or a feature
 request for the case of exit status 3) and may be reported on
 Frama-C\[cq]s BTS (see below).
 .SH ENVIRONMENT VARIABLES
-.PP
 It is possible to control the places where Frama-C looks for its files
 through the following variables.
 .TP
@@ -644,7 +638,6 @@ FRAMAC_SHARE
 The directory where Frama-C data (e.g.\ its version of the standard
 library) is installed.
 .SH SEE ALSO
-.PP
 Frama-C user manual:
 https://frama-c.com/download/frama-c-user-manual.pdf
 .PP
diff --git a/man/frama-c.1.md b/man/frama-c.1.md
index b793a002f499dcc035e0388103b471c23b88d6fa..9b4007641b51fedc8f0c62a42913e9fc58d6867d 100644
--- a/man/frama-c.1.md
+++ b/man/frama-c.1.md
@@ -260,8 +260,12 @@ Defaults to no.
 [-no]-keep-switch
 : when **-simplify-cfg** is set, keeps switch statements. Defaults to no.
 
--keep-unused-specified-functions
-: see **-remove-unused-specified-functions**.
+-keep-unused-functions *criterion*
+: keeps or removes function prototypes for functions that have no body and
+are not used. *criterion* is one of: **none**, **specified**, **all**, and
+**all_debug**; **specified** (the default value) keeps function prototypes
+that have an ACSL specification. **all** and **all_debug** are identical except
+for compiler builtins, which are only included with **all_debug**.
 
 -keep-unused-types
 : see **-remove-unused-types**.
@@ -387,11 +391,6 @@ functions were fully inlined.
 : removes the given projects *p1,...,pn*.
 **@all_but_current** removes all projects but the current one.
 
--remove-unused-specified-functions
-: keeps function prototypes that have an ACSL specification but are not used
-in the code. This is the default. Functions having the attribute
-**FRAMAC_BUILTIN** are always kept.
-
 -remove-unused-types
 : remove types and struct/union/enum declarations that are not referenced
 anywhere else in the code. This is the default. Use **-keep-unused-types**
diff --git a/src/kernel_services/ast_data/ast.ml b/src/kernel_services/ast_data/ast.ml
index 5dbe5309e22766f5b5793b08ac3550a6761d88c8..05a5e0158e7026370dcd79e5a2e6dde44e79aa13 100644
--- a/src/kernel_services/ast_data/ast.ml
+++ b/src/kernel_services/ast_data/ast.ml
@@ -39,7 +39,7 @@ include
           Kernel.PreprocessAnnot.self;
           Kernel.Files.self;
           Kernel.UnfoldingLevel.self;
-          Kernel.Keep_unused_specified_functions.self;
+          Kernel.KeepUnusedFunctions.self;
           Kernel.Keep_unused_types.self;
           Cil.selfFormalsDecl ]
     end)
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index ad01c4a10bd0ba58dfc305d162c260c6068ae3f3..24615768362c0e13990a0290256f6203ac723b56 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -662,17 +662,19 @@ let () =
    other unused globals according to relevant command-line parameters.
    This function is meant to be passed to {!Rmtmps.removeUnused}. *)
 let isRoot g =
-  let specs = Kernel.Keep_unused_specified_functions.get () in
+  let keepFuncs = Kernel.KeepUnusedFunctions.get () in
   let keepTypes = Kernel.Keep_unused_types.get () in
   Rmtmps.isExportedRoot g ||
   match g with
   | GFun({svar = v; sspec = spec},_)
   | GFunDecl(spec,v,_) ->
+    (* Always keep the declaration of the entry point... *)
     Kernel.MainFunction.get_plain_string () = v.vname
-    (* Always keep the declaration of the entry point *)
-    || (specs && not (is_empty_funspec spec))
-  (* and the declarations carrying specifications according to the
-     command line.*)
+    (* ... and the declarations of unused functions according to
+       the command-line option *)
+    || keepFuncs = "all_debug"
+    || (keepFuncs = "all" && not (Cil_builtins.Builtin_functions.mem v.vname))
+    || (keepFuncs = "specified" && not (is_empty_funspec spec))
   | GType _ | GCompTag _ | GCompTagDecl _ | GEnumTag _ | GEnumTagDecl _ ->
     keepTypes
   | _ -> false
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 73cf18ce7ce6c6d819a0edfd36438dda468d6fee..fdc4828f50e784b01d34b48f7dd99b09972c93a1 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -1346,13 +1346,19 @@ module KeepSwitch =
   end)
 
 let () = Parameter_customize.set_group normalisation
-let () = Parameter_customize.set_negative_option_name "-remove-unused-specified-functions"
-module Keep_unused_specified_functions =
-  True(struct
-    let option_name = "-keep-unused-specified-functions"
-    let module_name = "Keep_unused_specified_functions"
-    let help = "keep specified-but-unused functions"
+module KeepUnusedFunctions =
+  String(struct
+    let module_name = "KeepUnusedFunctions"
+    let option_name = "-keep-unused-functions"
+    let default = "specified"
+    let arg_name = "none|specified|all|all_debug"
+    let help = "whether to keep unused function declarations: none, \
+                only functions with specifications (by default), \
+                or keep all unused functions (all_debug also includes \
+                compiler builtins)"
   end)
+let () = KeepUnusedFunctions.set_possible_values ["none"; "specified"; "all";
+                                                  "all_debug"]
 
 let () = Parameter_customize.set_group normalisation
 let () = Parameter_customize.set_negative_option_name "-remove-unused-types"
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index 2e8856d2e52a1be2828459e7d8946faeacd7d2f3..c0359ebf232f021d47ad6ac2c60958c5f88036a4 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -501,8 +501,8 @@ module SimplifyCfg: Parameter_sig.Bool
 module KeepSwitch: Parameter_sig.Bool
 (** Behavior of option "-keep-switch" *)
 
-module Keep_unused_specified_functions: Parameter_sig.Bool
-(** Behavior of option "-keep-unused-specified-functions". *)
+module KeepUnusedFunctions: Parameter_sig.String
+(** Behavior of option "-keep-unused-functions". *)
 
 module Keep_unused_types: Parameter_sig.Bool
 (** Behavior of option "-keep-unused-types". *)
diff --git a/src/plugins/e-acsl/doc/userman/provides.tex b/src/plugins/e-acsl/doc/userman/provides.tex
index 5080d6b62c25dc49d12433cae7e0d8485a4ca96f..2b93a88fa708b942a52d400a9331579e42d0f96f 100644
--- a/src/plugins/e-acsl/doc/userman/provides.tex
+++ b/src/plugins/e-acsl/doc/userman/provides.tex
@@ -330,7 +330,7 @@ folder of \framac and \texttt{\$E\_ACSL\_LIB} points to the
 \texttt{lib/frama-c/e-acsl} folder of \framac):
 \begin{frama-c-commands}
   \$ frama-c \
-        -remove-unused-specified-functions \
+        -keep-unused-functions none \
         -machdep gcc_x86_64 \
         -cpp-extra-args="-std=c99 -D_DEFAULT_SOURCE -D__NO_CTYPE \
                          -D__FC_MACHDEP_X86_64" \
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
index 68880f34d5403caff56eaa5b9578ded731a0f258..ebab561f7c4a108a8b6c5532e4ca539742b73fe5 100755
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
@@ -1041,7 +1041,7 @@ fi
 
 # Extra Frama-C Flags E-ACSL needs
 FRAMAC_FLAGS="$FRAMAC_FLAGS \
-  -remove-unused-specified-functions"
+  -keep-unused-functions none"
 
 if [ -n "$OPTION_VALIDATE_FORMAT_STRINGS" ]; then
   FRAMAC_FLAGS="$FRAMAC_FLAGS \
diff --git a/src/plugins/e-acsl/src/options.ml b/src/plugins/e-acsl/src/options.ml
index 506c123ac28a3cd6cd329d3c0064f55704082f73..c7bf82aaae253be85e7a37bc16454e3b01f4ccee 100644
--- a/src/plugins/e-acsl/src/options.ml
+++ b/src/plugins/e-acsl/src/options.ml
@@ -293,7 +293,7 @@ let setup ?(rtl=false) () =
   end;
   (* Additionnal kernel options while parsing the RTL project. *)
   if rtl then begin
-    Kernel.Keep_unused_specified_functions.off ();
+    Kernel.KeepUnusedFunctions.set "none";
     Kernel.CppExtraArgs.add
       (Format.asprintf " -DE_ACSL_MACHDEP=%s" (Kernel.Machdep.get ()));
   end
diff --git a/src/plugins/e-acsl/tests/test_config b/src/plugins/e-acsl/tests/test_config
index a729d3877fc2389a3b8497ade9c3f68750616abd..c779520777bc7fbcb06875e071ad7a89f1b5bdbe 100644
--- a/src/plugins/e-acsl/tests/test_config
+++ b/src/plugins/e-acsl/tests/test_config
@@ -1,6 +1,6 @@
 MACRO: DEST @PTEST_RESULT@/gen_@PTEST_NAME@
 MACRO: MACHDEP -machdep gcc_x86_64
-MACRO: GLOBAL @MACHDEP@ -remove-unused-specified-functions -verbose 0 -no-unicode
+MACRO: GLOBAL @MACHDEP@ -keep-unused-functions none -verbose 0 -no-unicode
 
 COMMENT: no more share to set with Dune
 MACRO: EACSL -e-acsl -e-acsl-verbose 1
diff --git a/tests/spec/unused.c b/tests/spec/unused.c
index ab8202675f70303966352116061bba32ce01ffbf..4de4879af97288ee96c8b9923d01cfaf9e64d547 100644
--- a/tests/spec/unused.c
+++ b/tests/spec/unused.c
@@ -1,5 +1,5 @@
 /* run.config
-STDOPT: +"-remove-unused-specified-functions" +"-kernel-msg-key printer:builtins"
+STDOPT: +"-keep-unused-functions none" +"-kernel-msg-key printer:builtins"
 */
 typedef struct { int i; } T;