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.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;