From 334951cd1c4052f8e55142782ddfa8650f769f84 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 7 May 2024 16:33:29 +0200
Subject: [PATCH] [Kernel] rename and extend -remove-unused-specified-functions
as -keep-unused-functions
---
doc/userman/user-changes.tex | 8 +++++++-
doc/userman/user-sources.tex | 14 ++++++++++----
man/frama-c.1.md | 13 ++++++-------
src/kernel_services/ast_data/ast.ml | 2 +-
src/kernel_services/ast_queries/file.ml | 12 +++++++-----
.../plugin_entry_points/kernel.ml | 18 ++++++++++++------
.../plugin_entry_points/kernel.mli | 4 ++--
src/plugins/e-acsl/doc/userman/provides.tex | 2 +-
src/plugins/e-acsl/scripts/e-acsl-gcc.sh | 2 +-
src/plugins/e-acsl/src/options.ml | 2 +-
src/plugins/e-acsl/tests/test_config | 2 +-
tests/spec/unused.c | 2 +-
12 files changed, 50 insertions(+), 31 deletions(-)
diff --git a/doc/userman/user-changes.tex b/doc/userman/user-changes.tex
index b2868d04b70..b3a1cd537ad 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 2fb46c26613..6b6fbb73637 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 b793a002f49..9b4007641b5 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 5dbe5309e22..05a5e0158e7 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 ad01c4a10bd..24615768362 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 73cf18ce7ce..fdc4828f50e 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 2e8856d2e52..c0359ebf232 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 5080d6b62c2..2b93a88fa70 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 68880f34d54..ebab561f7c4 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 506c123ac28..c7bf82aaae2 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 a729d3877fc..c779520777b 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 ab8202675f7..4de4879af97 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;
--
GitLab