From 6d9dc0a5e98afb171ffde5f88e38fa7228ab891c Mon Sep 17 00:00:00 2001 From: Andre Maroneze <andre.oliveiramaroneze@cea.fr> Date: Tue, 26 May 2020 14:02:13 +0200 Subject: [PATCH] [Doc] fix several occurrences of un-idiomatic English --- doc/userman/user-sources.tex | 2 +- doc/userman/user-start.tex | 2 +- doc/value/main.tex | 2 +- man/frama-c.1.md | 2 +- src/kernel_services/ast_queries/file.mli | 2 +- src/kernel_services/ast_queries/json_compilation_database.ml | 2 +- src/plugins/metrics/metrics_cilast.ml | 2 +- 7 files changed, 7 insertions(+), 7 deletions(-) diff --git a/doc/userman/user-sources.tex b/doc/userman/user-sources.tex index fe3dce5597b..3d049acfa9f 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 2fb137f37cb..099980681bb 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 0afcb450bff..d74d11da488 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 fd594ab8978..396cf3138d6 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 ab713a012fe..f92e9ad97db 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 4d2c1eb41af..4f8eaa440ef 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 e7b4c4e4741..c6a607be5d6 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) -- GitLab