diff --git a/doc/userman/user-services.tex b/doc/userman/user-services.tex index cc1f485ba93790d1588952824de815faa6ac469f..24aca42be20f94c4c5714a43cd1ca11ecbb66cc6 100644 --- a/doc/userman/user-services.tex +++ b/doc/userman/user-services.tex @@ -89,7 +89,7 @@ loading another project file. Options \optionuse{-}{help}, \optionuse{-}{verbose}, \optionuse{-}{debug}\xspace(and their corresponding plugin-specific counterpart) -as well as \optionuse{-}{quiet}\xspace and +as well as \optionuse{-}{explain}, \optionuse{-}{quiet}\xspace and \optionuse{-}{unicode}\xspace are not saved on disk. \section{Dependencies between Analyses} @@ -185,5 +185,5 @@ generates (resp. does not generate) a journal upon exiting the session. Modifications of options \optionuse{-}{help}, \optionuse{-}{verbose}, \optionuse{-}{debug}\xspace (and their corresponding counterpart) as well as -\optionuse{-}{quiet}\xspace and \optionuse{-}{unicode}\xspace are not written in -the journal. +\optionuse{-}{explain}, \optionuse{-}{quiet}\xspace and +\optionuse{-}{unicode}\xspace are not written in the journal. diff --git a/doc/userman/user-sources.tex b/doc/userman/user-sources.tex index fe3dce5597bd0bb76bc0ffe7129072fbb23a4a99..3d049acfa9f33a54c89ba778fe0fe4c1265c5cab 100644 --- a/doc/userman/user-sources.tex +++ b/doc/userman/user-sources.tex @@ -99,7 +99,7 @@ as if they had been manually added via \texttt{-cpp-extra-args-per-file}. Note: if both \texttt{-cpp-extra-args-per-file} and the JSON compilation database specify options for a given file, the former are used and the latter are ignored. Also note that the use of the database simply adds flags -{\em for the files specified in the command-line}, but these files must still +{\em for the files specified on the command-line}, but these files must still be specified by the user. In all of the above cases, diff --git a/doc/userman/user-start.tex b/doc/userman/user-start.tex index c90a579eeee645e3c8f9a1473db378e5c7d3c3ed..099980681bbc7495273ca9b0a0e83435773c346d 100644 --- a/doc/userman/user-start.tex +++ b/doc/userman/user-start.tex @@ -132,6 +132,10 @@ while \optiondef{-}{version} prints the \FramaC version only The options of the installed plug-ins are displayed by using either the option \texttt{-<plug-in shortname>-help} or \texttt{-<plug-in shortname>-h}. +Finally, the option \optiondef{-}{explain} can be used to obtain information +about some specific options of the kernel or of any installed plug-ins: +it prints a help message for each other option given on the command line. + \subsection{\FramaC Configuration}\label{sec:version} The complete configuration of \FramaC can be obtained with various options, diff --git a/doc/value/main.tex b/doc/value/main.tex index 0afcb450bff549d6154ee7f9f9d44de778deaae3..d74d11da48850182dd592cf982d22195cc6ce37a 100644 --- a/doc/value/main.tex +++ b/doc/value/main.tex @@ -504,7 +504,7 @@ This call to \verb|printf| has no observable effects for the analysis anyway, so we do not have anything to be concerned with. It is still a good idea to check the specification of each function without body used during the analysis, since the overall correctness depends on them. This can be done using the -GUI or, in the command line, with option \verb|-print|, which outputs the +GUI or, on the command line, with option \verb|-print|, which outputs the Frama-C normalized source code, including ACSL specifications and transformations performed by the \textsf{Variadic} plugin. diff --git a/man/frama-c.1.md b/man/frama-c.1.md index 319c04fc20a3670566a429c73c2393888942264f..396cf3138d6b15f78d2354d2b41a5767104c8bc8 100644 --- a/man/frama-c.1.md +++ b/man/frama-c.1.md @@ -55,6 +55,9 @@ option which has the opposite effect. -kernel-help : prints the list of options recognized by Frama-C's kernel +-explain +: prints a help message for each other option given on the command line + -verbose *n* : sets verbosity level. Defaults to 1. Setting it to 0 will output less progress messages. diff --git a/src/kernel_services/ast_queries/file.mli b/src/kernel_services/ast_queries/file.mli index ab713a012fe2d70480d05cfdb750bdb874e6c10b..f92e9ad97db69f4b205b941c026b81843a8c34ce 100644 --- a/src/kernel_services/ast_queries/file.mli +++ b/src/kernel_services/ast_queries/file.mli @@ -28,7 +28,7 @@ type cpp_opt_kind = Gnu | Not_gnu | Unknown (** File type, according to how it will be preprocessed. Note: [string] is used here instead of [Filepath], to preserve - names given in the command line, without normalization. *) + names given on the command line, without normalization. *) type file = | NeedCPP of Filepath.Normalized.t * string * cpp_opt_kind (** The first string is the filename of the [.c] to preprocess. diff --git a/src/kernel_services/ast_queries/json_compilation_database.ml b/src/kernel_services/ast_queries/json_compilation_database.ml index 4d2c1eb41afe3b1bd1eebeda3ba8c13097bb1ff1..4f8eaa440efe9c2c426797e6df47e2ae1be306c0 100644 --- a/src/kernel_services/ast_queries/json_compilation_database.ml +++ b/src/kernel_services/ast_queries/json_compilation_database.ml @@ -175,7 +175,7 @@ let parse_entry ?(cwd=Sys.getcwd()) r = | Undefine s -> s ^ suffix in (* we must process the arguments in-order, since several -D and -U may - exist in the command line *) + exist on the command line *) (* prev is the prefix of the previous argument (if any) *) let _, res = List.fold_left (fun (prev, acc_res) arg -> diff --git a/src/kernel_services/cmdline_parameters/cmdline.ml b/src/kernel_services/cmdline_parameters/cmdline.ml index 5a166f93f07e86f6225bc60ab3f9edc10a7d8f23..808046e9e9180b7639fc2a73fe8091dfd354cae5 100644 --- a/src/kernel_services/cmdline_parameters/cmdline.ml +++ b/src/kernel_services/cmdline_parameters/cmdline.ml @@ -436,6 +436,7 @@ module Plugin: sig short: string; groups: (string, cmdline_option list ref) Hashtbl.t } val all_plugins: unit -> t list + val all_options: (string, cmdline_option) Hashtbl.t val add: ?short:string -> string -> help:string -> unit val add_group: ?memo:bool -> plugin:string -> string -> string * bool val add_option: string -> group:string -> cmdline_option -> unit @@ -459,6 +460,9 @@ end = struct (* all the registered plug-ins indexed by their shortnames *) let plugins : (string, t) Hashtbl.t = Hashtbl.create 17 + (* all the registered options indexed by their name. *) + let all_options : (string, cmdline_option) Hashtbl.t = Hashtbl.create 97 + let all_plugins () = let cmp p1 p2 = Extlib.compare_ignore_case p1.name p2.name in List.sort cmp (Hashtbl.fold (fun _ p acc -> p :: acc) plugins []) @@ -518,6 +522,7 @@ end = struct let add_option shortname ~group option = assert (option.oname <> ""); + Hashtbl.replace all_options option.oname option; Option_names.add option.oname false; let g = find_group shortname group in g := option :: !g @@ -531,6 +536,7 @@ end = struct let option = List.find (fun o -> o.oname = orig) !options_group in let get_one name = 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 options_group := alias :: !options_group; @@ -1072,6 +1078,46 @@ let list_all_plugin_options ~print_invisible = end; raise Exit +(* ************************************************************************* *) +(** {3 Explain} + + Special processing for option "-explain" *) +(* ************************************************************************* *) + +let pp_option_help name = + try + let option = Hashtbl.find Plugin.all_options name in + let help = + if option.oname = name then option.ohelp else + "alias for " ^ option.oname ^ "\n" ^ option.ohelp + in + let argname = option.argname in + let name = if argname = "" then name else name ^ " <" ^ argname ^ ">" in + let print fmt = print_helpline fmt name help option.ext_help in + Log.print_on_output print + with Not_found -> + let print fmt = Format.fprintf fmt "Invalid option %s@." name in + Log.print_on_output print + +(* [option_re] allows matching an option and extracting its name, + even when there is a '=', e.g. "-kernel-msg-key=-typing". + It also prevents matching negative numbers, as in "-ulevel -1". *) +let option_re = Str.regexp "-\\([a-zA-Z-][a-zA-Z0-9-]*\\)" +let explain_cmdline () = + let option_names = + List.fold_left + (fun acc option -> + if Str.string_match option_re option 0 && option <> "-explain" + then Str.matched_string option :: acc + else acc) + [] all_options + in + Log.print_on_output + (fun fmt -> + Format.fprintf fmt "[kernel] Explaining command-line options:@."); + List.iter pp_option_help (List.rev option_names); + raise Exit + (* Local Variables: compile-command: "make -C ../../.." diff --git a/src/kernel_services/cmdline_parameters/cmdline.mli b/src/kernel_services/cmdline_parameters/cmdline.mli index 1d25f445994d2949941459347f478b4c30670d55..db33fb745847cabe9fa7b88dc972026eb8f64eaa 100644 --- a/src/kernel_services/cmdline_parameters/cmdline.mli +++ b/src/kernel_services/cmdline_parameters/cmdline.mli @@ -244,6 +244,8 @@ val list_plugins: unit -> exit @since Phosphorus-20170501-beta1 *) val list_all_plugin_options : print_invisible:bool -> exit +val explain_cmdline : unit -> exit + val plugin_help: string -> exit (** Display the help of the given plug-in (given by its shortname). @since Beryllium-20090601-beta1 *) diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml index 1590e44022fb7b4c9423c25c5137d9f268c5ea17..da63179bf0fa0632cd2a51a10eafeff0dc914419 100644 --- a/src/kernel_services/plugin_entry_points/kernel.ml +++ b/src/kernel_services/plugin_entry_points/kernel.ml @@ -429,6 +429,26 @@ let run_list_all_plugin_options () = else Cmdline.nop let () = Cmdline.run_after_exiting_stage run_list_all_plugin_options +let () = Parameter_customize.set_group help +let () = Parameter_customize.set_cmdline_stage Cmdline.Extending +let () = Parameter_customize.do_not_journalize () +let () = Parameter_customize.set_negative_option_name "" +module Explain = + False + (struct + let option_name = "-explain" + let help = "prints the help message for each option given in the \ + command line" + let module_name = "Explain" + end) + +let () = + Cmdline.run_after_exiting_stage (fun () -> + if Explain.get () then Cmdline.explain_cmdline () + else Cmdline.nop) +(* This option is processed in a special manner in [Cmdline]. + Nothing to be done here. *) + (* ************************************************************************* *) (** {2 Output Messages} *) (* ************************************************************************* *) diff --git a/src/plugins/metrics/metrics_cilast.ml b/src/plugins/metrics/metrics_cilast.ml index e7b4c4e4741a4440a8c5934c5926094a478c747d..c6a607be5d638141e0d2269cd2a6ce2a5d1a66d8 100644 --- a/src/plugins/metrics/metrics_cilast.ml +++ b/src/plugins/metrics/metrics_cilast.ml @@ -493,7 +493,7 @@ let used_files () = let pretty_used_files used_files = (* Note: used_files may also contain #include'd files, - but we only want those given in the command line *) + but we only want those given on the command line *) let cmdline_files = List.fold_left (fun acc file -> Datatype.Filepath.Set.add ( Datatype.Filepath.of_string (Kernel_file.get_name file)