Commit 9e7f7673 authored by Michele Alberti's avatar Michele Alberti
Browse files

Merge branch 'feature/eva/deprecated-aliases' into 'master'

[Eva] Deprecate legacy parameters aliases

See merge request frama-c/frama-c!2815
parents 436eac2a 32029606
......@@ -253,6 +253,11 @@ type option_setting =
| Int of (int -> unit)
| String of (string -> unit)
let option_setting_and_warn warn = function
| Unit f -> Unit (fun () -> warn (); f ())
| Int f -> Int (fun i -> warn (); f i)
| String f -> String (fun s -> warn (); f s)
exception Cannot_parse of string * string
let raise_error name because = raise (Cannot_parse(name, because))
......@@ -436,7 +441,8 @@ module Plugin: sig
val add_group: ?memo:bool -> plugin:string -> string -> string * bool
val add_option: string -> group:string -> cmdline_option -> unit
val add_aliases:
orig:string -> string -> group:string -> string list -> cmdline_option list
orig:string -> string -> group:string -> ?visible:bool -> ?deprecated:bool
-> string list -> cmdline_option list
val replace_option_setting:
string -> plugin:string -> group:string -> option_setting -> unit
val replace_option_help:
......@@ -525,7 +531,7 @@ end = struct
(* table name_of_the_original_option --> aliases *)
let aliases_tbl = Hashtbl.create 7
let add_aliases ~orig shortname ~group names =
let add_aliases ~orig shortname ~group ?(visible=true) ?(deprecated=false) names =
(* mostly inline [add_option] and perform additional actions *)
let options_group = find_group shortname group in
let option = List.find (fun o -> o.oname = orig) !options_group in
......@@ -533,7 +539,19 @@ end = struct
if name = "" then invalid_arg "empty alias name";
Hashtbl.replace all_options name option;
Option_names.add name true;
let alias = { option with oname = name } in
let setting =
if deprecated
then
let warn () =
Kernel_log.warning ~once:true
"@[%s is@ a deprecated alias@ for option %s.@ \
Please use %s instead.@]"
name option.oname option.oname
in
option_setting_and_warn warn option.setting
else option.setting
in
let alias = { option with oname = name; ovisible = visible; setting; } in
options_group := alias :: !options_group;
alias
in
......@@ -723,8 +741,8 @@ let add_option_without_action
ohelp = help; ext_help = ext_help; ovisible = visible;
setting = Unit (fun () -> assert false) }
let add_aliases orig ~plugin ~group stage aliases =
let l = Plugin.add_aliases ~orig plugin ~group aliases in
let add_aliases orig ~plugin ~group ?visible ?deprecated stage aliases =
let l = Plugin.add_aliases ~orig plugin ~group ?visible ?deprecated aliases in
let add = match stage with
| Early -> Early_Stage.add_for_parsing
| Extending -> Extending_Stage.add_for_parsing
......@@ -899,7 +917,8 @@ let low_print_option_help fmt print_invisible o =
print_helpline fmt (name ^ ty) o.ohelp o.ext_help;
List.iter
(fun o ->
print_helpline fmt (o.oname ^ ty) ("alias for option " ^ name) "")
if print_invisible || o.ovisible then
print_helpline fmt (o.oname ^ ty) ("alias for option " ^ name) "")
(Plugin.find_option_aliases o)
end;
true
......
......@@ -313,13 +313,18 @@ val add_aliases:
string ->
plugin:string ->
group:Group.t ->
?visible: bool ->
?deprecated: bool ->
stage ->
string list ->
unit
(** [add_aliases orig plugin group aliases] adds a list of aliases to the given
option name [orig].
If [visible] is set to false, the aliases do not appear in help messages.
If [deprecated] is set to true, the use of the aliases emits a warning.
@Invalid_argument if an alias name is the empty string
@since Carbon-20110201 *)
@since Carbon-20110201
@modify Frama-c+dev add [visible] and [deprecated] arguments. *)
val replace_option_setting:
string -> plugin:string -> group:Group.t -> option_setting -> unit
......
......@@ -223,14 +223,15 @@ struct
~plugin X.option_name Typed_parameter.ty ~journalize:false p
else p
let add_aliases list =
add_aliases list;
let add_aliases ?visible ?deprecated list =
add_aliases ?visible ?deprecated list;
match !negative_option_ref with
| None -> ()
| Some negative_option ->
let negative_list = List.map negate_name list in
let plugin = P.shortname in
Cmdline.add_aliases negative_option ~plugin ~group stage negative_list
Cmdline.add_aliases
negative_option ~plugin ~group ?visible ?deprecated stage negative_list
end
......@@ -1719,8 +1720,8 @@ struct
f ();
end
let add_aliases list =
add_aliases list;
let add_aliases ?visible ?deprecated list =
add_aliases ?visible ?deprecated list;
Output.add_aliases (List.map (fun alias -> alias ^ "-print") list)
end
......
......@@ -179,10 +179,13 @@ module type S_no_parameter = sig
val equal: t -> t -> bool
val add_aliases: string list -> unit
val add_aliases: ?visible: bool -> ?deprecated:bool -> string list -> unit
(** Add some aliases for this option. That is other option names which have
exactly the same semantics that the initial option.
@raise Invalid_argument if one of the strings is empty *)
If [visible] is set to false, the aliases do not appear in help messages.
If [deprecated] is set to true, the use of the aliases emits a warning.
@raise Invalid_argument if one of the strings is empty
@modify Frama-c+dev add [visible] and [deprecated] arguments. *)
(**/**)
val is_set: unit -> bool
......
......@@ -270,8 +270,9 @@ struct
let option_name = X.option_name
let add_aliases =
Cmdline.add_aliases option_name ~plugin:P.shortname ~group stage
let add_aliases ?visible ?deprecated =
Cmdline.add_aliases
option_name ~plugin:P.shortname ~group stage ?visible ?deprecated
let print_help fmt =
Cmdline.print_option_help fmt ~plugin:P.shortname ~group option_name
......
......@@ -44,7 +44,8 @@ module type S_no_log = sig
module Config: Parameter_sig.Specific_dir
val help: Cmdline.Group.t
val messages: Cmdline.Group.t
val add_plugin_output_aliases: string list -> unit
val add_plugin_output_aliases:
?visible:bool -> ?deprecated:bool -> string list -> unit
end
module type S = sig
......@@ -795,14 +796,14 @@ struct
let is_kernel = is_kernel () in
Warn_category.add_set_hook (parse_warn_directives is_kernel)
let add_plugin_output_aliases aliases =
let add_plugin_output_aliases ?visible ?deprecated aliases =
let aliases = List.filter (fun alias -> alias <> "") aliases in
let optname suffix = List.map (fun alias -> "-" ^ alias ^ suffix) aliases in
Help.add_aliases (optname "-help");
Verbose.add_aliases (optname "-verbose");
Debug_category.add_aliases (optname "-msg-key");
Warn_category.add_aliases (optname "-warn-key");
LogToFile.add_aliases (optname "-log")
Help.add_aliases ?visible ?deprecated (optname "-help");
Verbose.add_aliases ?visible ?deprecated (optname "-verbose");
Debug_category.add_aliases ?visible ?deprecated (optname "-msg-key");
Warn_category.add_aliases ?visible ?deprecated (optname "-warn-key");
LogToFile.add_aliases ?visible ?deprecated (optname "-log")
let () = reset_plugin ()
......
......@@ -64,12 +64,14 @@ module type S_no_log = sig
(** The group containing options -*-debug and -*-verbose.
@since Boron-20100401 *)
val add_plugin_output_aliases: string list -> unit
(** Adds aliases to the options -plugin-help, -plugin-verbose, -plugin-log,
-plugin-msg-key, and -plugin-warn-key.
[add_plugin_output_aliases [alias]] adds the aliases -alias-help,
-alias-verbose, etc.
@since 18.0-Argon *)
val add_plugin_output_aliases:
?visible:bool -> ?deprecated:bool -> string list -> unit
(** Adds aliases to the options -plugin-help, -plugin-verbose, -plugin-log,
-plugin-msg-key, and -plugin-warn-key.
[add_plugin_output_aliases [alias]] adds the aliases -alias-help,
-alias-verbose, etc.
@since 18.0-Argon
@modify Frama-c+dev add [visible] and [deprecated] arguments. *)
end
(** Provided plug-general services for plug-ins.
......
/* run.config_ci
COMMENT: arrays
STDOPT: #"-slevel 5"
STDOPT: #"-eva-slevel 5"
*/
int T1[3],T2[4];
......@@ -113,4 +113,4 @@ int main(void) {
vlas(3);
return 0;
}
\ No newline at end of file
}
/* run.config_ci
COMMENT: invariant
STDOPT: +"-slevel 11"
STDOPT: +"-eva-slevel 11"
*/
int main(void) {
......
/* run.config_ci
COMMENT: loop invariants
STDOPT: +"-slevel 160"
STDOPT: +"-eva-slevel 160"
*/
void simple_loop() {
......
/*run.config
OPT: -no-autoload-plugins -load-module from,inout,loopanalysis,eva,scope -val -val-show-progress -then -loop
OPT: -no-autoload-plugins -load-module from,inout,loopanalysis,eva,scope -eva -eva-show-progress -then -loop
*/
void f1(int n) {
......
/* run.config
STDOPT: #"-val-builtin strlen:Frama_C_strlen"
STDOPT: #"-eva-builtin strlen:Frama_C_strlen"
*/
#include <string.h>
......
/* run.config
STDOPT: #"-val-builtin memcpy:Frama_C_memcpy"
STDOPT: #"-eva-builtin memcpy:Frama_C_memcpy"
*/
#include <string.h>
......
OPT: -no-autoload-plugins -load-module from,inout,nonterm,scope -val -val-show-progress -eva-msg-key=-summary -then -nonterm -nonterm-verbose 2
OPT: -no-autoload-plugins -load-module from,inout,nonterm,scope -eva -eva-show-progress -eva-msg-key=-summary -then -nonterm -nonterm-verbose 2
/* run.config
LOG: csv.csv
OPT: -no-autoload-plugins -load-module from,inout,report,scope,eva -eva-warn-copy-indeterminate=-main4 -eva -eva-show-progress -remove-redundant-alarms -eva-warn-key=alarm=inactive -then -report-csv @PTEST_RESULT@/csv.csv -report-no-proven -then -report-csv= -eva-warn-key=alarm -slevel 1
OPT: -no-autoload-plugins -load-module from,inout,report,scope,eva -eva-warn-copy-indeterminate=-main4 -eva -eva-show-progress -eva-remove-redundant-alarms -eva-warn-key=alarm=inactive -then -report-csv @PTEST_RESULT@/csv.csv -report-no-proven -then -report-csv= -eva-warn-key=alarm -eva-slevel 1
COMMENT: first, do an analysis without any message, but check that the .csv is complete. Then, redo the analysis with value warnings. slevel 1 is just there to force Value to restart
*/
volatile v;
......
OPT: -val -journal-disable -out -input -deps
OPT: -eva -journal-disable -out -input -deps
This diff is collapsed.
......@@ -131,12 +131,10 @@ module SplitReturnFunction:
module SplitGlobalStrategy: State_builder.Ref with type data = Split_strategy.t
module ValShowProgress: Parameter_sig.Bool
module ValShowInitialState: Parameter_sig.Bool
module ValShowPerf: Parameter_sig.Bool
module ValPerfFlamegraphs: Parameter_sig.String
module ShowSlevel: Parameter_sig.Int
module PrintCallstacks: Parameter_sig.Bool
module AlarmsWarnings: Parameter_sig.Bool
module ReportRedStatuses: Parameter_sig.String
module NumerorsLogFile: Parameter_sig.String
......
/* run.config
STDOPT: +"-no-val-alloc-returns-null"
STDOPT: +"-eva-no-alloc-returns-null"
*/
......
/* run.config
STDOPT: +"-no-val-alloc-returns-null"
STDOPT: +"-eva-no-alloc-returns-null"
*/
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment