From b66d381e75fd03c2ef6dc1a72b8dbb8da7243b58 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr> Date: Tue, 16 Apr 2024 20:44:55 +0200 Subject: [PATCH] [Impact] Renames option -impact-pragma into -impact-annot. -impact-pragma remains as an invisible deprecated alias of -impact-annot. --- doc/developer/advance.tex | 12 ++++++------ src/plugins/impact/options.ml | 9 +++++---- src/plugins/impact/options.mli | 4 ++-- src/plugins/impact/register.ml | 6 +++--- tests/impact/alias.i | 2 +- tests/impact/call.i | 6 +++--- tests/impact/called.i | 4 ++-- tests/impact/depend1.i | 2 +- tests/impact/depend2.i | 2 +- tests/impact/depend3.c | 2 +- tests/impact/depend4.i | 2 +- tests/impact/depend5.i | 2 +- tests/impact/first.i | 2 +- tests/impact/initial.i | 2 +- tests/impact/loop.i | 2 +- tests/impact/loop2.i | 2 +- tests/impact/slicing.i | 2 +- tests/impact/topbot.c | 2 +- tests/impact/undef_function.i | 2 +- tests/impact/variadic.i | 2 +- 20 files changed, 35 insertions(+), 34 deletions(-) diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex index 770627e22ec..0858a650b5b 100644 --- a/doc/developer/advance.tex +++ b/doc/developer/advance.tex @@ -2765,17 +2765,17 @@ module Print: Parameter_sig.Bool \end{ocamlcode} Another example is the parameter corresponding to the option -\texttt{-impact-pragma} of the plug-in \texttt{impact}. This parameter is -defined by the module \texttt{Pragma} (defined in the file +\texttt{-impact-annot} of the plug-in \texttt{impact}. This parameter is +defined by the module \texttt{Annot} (defined in the file \texttt{src/plugins/impact/options.ml}). It is implemented as follows. \sscodeidx{Parameter\_sig}{Builder}{Kernel\_function\_set} \begin{ocamlcode} -module Pragma = +module Annot = Kernel_function_set (struct - let option_name = "-impact-pragma" + let option_name = "-impact-annot" let arg_name = "f1, ..., fn" - let help = "use the impact pragmas in the code of functions f1,...,fn" + let help = "use the impact annotations in the code of functions f1,...,fn" end) \end{ocamlcode} Thus it is a set of \texttt{kernel\_function}s initialized by default to @@ -2785,7 +2785,7 @@ displaying help. The field \texttt{help} is the help message itself. The Interface for this module is simple: \scodeidx{Parameter\_sig}{Kernel\_function\_set} \begin{ocamlcode} -module Pragma: Parameter_sig.Kernel_function_set +module Annot: Parameter_sig.Kernel_function_set \end{ocamlcode} \end{example} diff --git a/src/plugins/impact/options.ml b/src/plugins/impact/options.ml index 8a089142eac..634fed1d126 100644 --- a/src/plugins/impact/options.ml +++ b/src/plugins/impact/options.ml @@ -27,13 +27,14 @@ include Plugin.Register let help = "impact analysis" end) -module Pragma = +module Annot = Kernel_function_set (struct - let option_name = "-impact-pragma" + let option_name = "-impact-annot" let arg_name = "f1, ..., fn" - let help = "use the impact pragmas in the code of functions f1,...,fn" + let help = "use the impact annotations in the code of functions f1,...,fn" end) +let () = Annot.add_aliases ~visible:false ~deprecated:true ["-impact-pragma"] module Print = False @@ -73,7 +74,7 @@ module Upward = let help = "compute compute impact in callers as well as in callees" end) -let is_on () = not (Pragma.is_empty ()) +let is_on () = not (Annot.is_empty ()) (* Local Variables: diff --git a/src/plugins/impact/options.mli b/src/plugins/impact/options.mli index faebc35aff1..8a56c311311 100644 --- a/src/plugins/impact/options.mli +++ b/src/plugins/impact/options.mli @@ -22,8 +22,8 @@ include Plugin.S -module Pragma: Parameter_sig.Kernel_function_set -(** Use pragmas of given function. *) +module Annot: Parameter_sig.Kernel_function_set +(** Use impact annotations of given function. *) module Print: Parameter_sig.Bool (** Print the impacted stmt on stdout. *) diff --git a/src/plugins/impact/register.ml b/src/plugins/impact/register.ml index ba41d38ea72..6de2b10f087 100644 --- a/src/plugins/impact/register.ml +++ b/src/plugins/impact/register.ml @@ -119,7 +119,7 @@ let compute_annots () = (* Returns the list of statements of function [kf] that have an impact annotation. *) let compute_impact_stmts kf acc = - (* Pragma option only accept defined functions. *) + (* Annot option only accept defined functions. *) let fundec = Kernel_function.get_definition kf in let has_impact_annot stmt = let impact_annots = Annotations.code_annot ~filter:is_impact_annot stmt in @@ -129,7 +129,7 @@ let compute_annots () = if impact_stmts = [] then acc else (kf, impact_stmts) :: acc in - let impact_stmts = Options.Pragma.fold compute_impact_stmts [] in + let impact_stmts = Options.Annot.fold compute_impact_stmts [] in let skip = Compute_impact.skip () in (* compute impact analyses on each kf *) let nodes = List.fold_left @@ -149,7 +149,7 @@ let from_nodes = compute_from_nodes let main () = if Options.is_on () then begin Options.feedback "beginning analysis"; - assert (not (Options.Pragma.is_empty ())); + assert (not (Options.Annot.is_empty ())); ignore (compute_annots ()); Options.feedback "analysis done" end diff --git a/tests/impact/alias.i b/tests/impact/alias.i index b44ead94109..593bd42ea9b 100644 --- a/tests/impact/alias.i +++ b/tests/impact/alias.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: +"-impact-pragma f" +"-lib-entry" +"-main f" +"-eva-remove-redundant-alarms" + STDOPT: +"-impact-annot f" +"-lib-entry" +"-main f" +"-eva-remove-redundant-alarms" */ int P,c; diff --git a/tests/impact/call.i b/tests/impact/call.i index 64ee9f379f3..65a046489c1 100644 --- a/tests/impact/call.i +++ b/tests/impact/call.i @@ -1,8 +1,8 @@ /* run.config - STDOPT: +"-impact-pragma main" - STDOPT: +"-impact-pragma main2" +"-main main2" - STDOPT: +"-impact-pragma main3" +"-main main3" + STDOPT: +"-impact-annot main" + STDOPT: +"-impact-annot main2" +"-main main2" + STDOPT: +"-impact-annot main3" +"-main main3" */ /*@ ghost int G; */ diff --git a/tests/impact/called.i b/tests/impact/called.i index db29ddef5c3..4c7aa54538b 100644 --- a/tests/impact/called.i +++ b/tests/impact/called.i @@ -1,6 +1,6 @@ /* run.config - STDOPT: +"-impact-pragma g" +"-lib-entry" +"-main g" - STDOPT: +"-impact-pragma h" +"-lib-entry" +"-main h" + STDOPT: +"-impact-annot g" +"-lib-entry" +"-main g" + STDOPT: +"-impact-annot h" +"-lib-entry" +"-main h" */ int X; diff --git a/tests/impact/depend1.i b/tests/impact/depend1.i index cb03869b56b..2a484acf570 100644 --- a/tests/impact/depend1.i +++ b/tests/impact/depend1.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: +"-impact-pragma main" + STDOPT: +"-impact-annot main" */ diff --git a/tests/impact/depend2.i b/tests/impact/depend2.i index 58b27ff58a5..902b09701d8 100644 --- a/tests/impact/depend2.i +++ b/tests/impact/depend2.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: +"-impact-pragma main" + STDOPT: +"-impact-annot main" */ int find(int x) { return x; } diff --git a/tests/impact/depend3.c b/tests/impact/depend3.c index 1eb4778f27c..2f30a06de0e 100644 --- a/tests/impact/depend3.c +++ b/tests/impact/depend3.c @@ -1,5 +1,5 @@ /* run.config - STDOPT: +"-impact-pragma main" + STDOPT: +"-impact-annot main" */ #define N 32 diff --git a/tests/impact/depend4.i b/tests/impact/depend4.i index 6368d46ea25..24d60d11a44 100644 --- a/tests/impact/depend4.i +++ b/tests/impact/depend4.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: +"-calldeps -then -impact-pragma main" + STDOPT: +"-calldeps -then -impact-annot main" */ int a, r1, r2; diff --git a/tests/impact/depend5.i b/tests/impact/depend5.i index e4800e4a54a..6b8869df18a 100644 --- a/tests/impact/depend5.i +++ b/tests/impact/depend5.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: #"@EVA_OPTIONS@ -calldeps -then -impact-pragma g" + STDOPT: #"@EVA_OPTIONS@ -calldeps -then -impact-annot g" */ int a, b, c, d, e; diff --git a/tests/impact/first.i b/tests/impact/first.i index d99654b37d5..74e17393458 100644 --- a/tests/impact/first.i +++ b/tests/impact/first.i @@ -1,6 +1,6 @@ /* run.config - STDOPT: +"-impact-pragma impact" +"-lib-entry" +"-main impact" + STDOPT: +"-impact-annot impact" +"-lib-entry" +"-main impact" */ int a, b, c, e, x, y, z, f, w; diff --git a/tests/impact/initial.i b/tests/impact/initial.i index 2d815c5edfb..a64c51e4b9a 100644 --- a/tests/impact/initial.i +++ b/tests/impact/initial.i @@ -1,6 +1,6 @@ /* run.config COMMENT: also tests the parsing of cmdline options of type string_set - STDOPT: +"-pdg-verbose 0" +"-main main1 -impact-pragma g1" +"-then -main main2 -impact-pragma='-@all,+g2'" +"-then -main main3 -impact-pragma='-g2,+g3'" + STDOPT: +"-pdg-verbose 0" +"-main main1 -impact-annot g1" +"-then -main main2 -impact-annot='-@all,+g2'" +"-then -main main3 -impact-annot='-g2,+g3'" */ int x1, x2, y2, z2, x3; diff --git a/tests/impact/loop.i b/tests/impact/loop.i index f1c26e9d35c..6099bb2803a 100644 --- a/tests/impact/loop.i +++ b/tests/impact/loop.i @@ -1,6 +1,6 @@ /* run.config - STDOPT: +"-impact-pragma loop" +"-lib-entry" +"-main loop" + STDOPT: +"-impact-annot loop" +"-lib-entry" +"-main loop" */ int c,x,y,z,w; diff --git a/tests/impact/loop2.i b/tests/impact/loop2.i index c6ff73de8e9..efe9f7fac61 100644 --- a/tests/impact/loop2.i +++ b/tests/impact/loop2.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: #"-impact-pragma main -lib-entry -calldeps" +"-then -ulevel 10" + STDOPT: #"-impact-annot main -lib-entry -calldeps" +"-then -ulevel 10" */ diff --git a/tests/impact/slicing.i b/tests/impact/slicing.i index 96b55a1278f..57d3eb073a3 100644 --- a/tests/impact/slicing.i +++ b/tests/impact/slicing.i @@ -1,6 +1,6 @@ /* run.config - STDOPT: +"-impact-pragma impact" +"-lib-entry" +"-main impact" +"-impact-slicing" +"-then-on 'impact slicing'" +"-print" + STDOPT: +"-impact-annot impact" +"-lib-entry" +"-main impact" +"-impact-slicing" +"-then-on 'impact slicing'" +"-print" */ int a, b, c, e, x, y, z, f, w; diff --git a/tests/impact/topbot.c b/tests/impact/topbot.c index 60b8397b97d..a86a7b4717f 100644 --- a/tests/impact/topbot.c +++ b/tests/impact/topbot.c @@ -1,5 +1,5 @@ /* run.config - STDOPT: +"-impact-pragma main -pdg -pdg-print" + STDOPT: +"-impact-annot main -pdg -pdg-print" */ //@ requires \false; diff --git a/tests/impact/undef_function.i b/tests/impact/undef_function.i index 156bd3e9f53..cb30fa6bf58 100644 --- a/tests/impact/undef_function.i +++ b/tests/impact/undef_function.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: +"-impact-pragma main" + STDOPT: +"-impact-annot main" */ int y; void g(int); diff --git a/tests/impact/variadic.i b/tests/impact/variadic.i index 3746a648146..3e0998336c2 100644 --- a/tests/impact/variadic.i +++ b/tests/impact/variadic.i @@ -1,6 +1,6 @@ /* run.config COMMENT: also tests the parsing of cmdline options of type string_set - STDOPT: +"-impact-pragma main" +"-then -main main1 -impact-pragma='-main,+main1'" +"-then -main main2 -impact-pragma='-@all,+main2'" +"-then -main main3 -impact-pragma='+aux3,-main2'" +"-then -main main4 -impact-pragma='-aux3,+aux4'" + STDOPT: +"-impact-annot main" +"-then -main main1 -impact-annot='-main,+main1'" +"-then -main main2 -impact-annot='-@all,+main2'" +"-then -main main3 -impact-annot='+aux3,-main2'" +"-then -main main4 -impact-annot='-aux3,+aux4'" */ int f(int, ...); -- GitLab