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