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 2fb137f37cb2bd8d0cbd8f32739e973cac502831..099980681bbc7495273ca9b0a0e83435773c346d 100644 --- a/doc/userman/user-start.tex +++ b/doc/userman/user-start.tex @@ -134,7 +134,7 @@ 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 in the command line. +it prints a help message for each other option given on the command line. \subsection{\FramaC Configuration}\label{sec:version} 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 fd594ab8978b16a1b826b39d655ce54c12cf4752..396cf3138d6b15f78d2354d2b41a5767104c8bc8 100644 --- a/man/frama-c.1.md +++ b/man/frama-c.1.md @@ -56,7 +56,7 @@ option which has the opposite effect. : prints the list of options recognized by Frama-C's kernel -explain -: prints a help message for each other option given in the command line +: prints a help message for each other option given on the command line -verbose *n* : sets verbosity level. Defaults to 1. 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/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)