From 20e7c0d95395156a4260681936115a0f89bfefad Mon Sep 17 00:00:00 2001 From: Andre Maroneze <andre.maroneze@cea.fr> Date: Mon, 9 Oct 2023 11:20:57 +0200 Subject: [PATCH] Normalize writing of 'preprocessor' The ISO C standard only uses the hyphen-less form, so we choose it by default. --- doc/aorai/SrcSchemas/GeneralView.fig | 2 +- doc/aorai/main.tex | 2 +- doc/developer/advance.tex | 4 ++-- doc/eva/main.tex | 8 +++---- doc/rte/rte.tex | 2 +- doc/userman/user-changes.tex | 2 +- doc/userman/user-intro.tex | 2 +- doc/userman/user-start.tex | 6 ++--- man/frama-c.1 | 22 +++++++++---------- man/frama-c.1.md | 22 +++++++++---------- .../parsing/logic_preprocess.mli | 10 ++++----- .../parsing/logic_preprocess.mll | 4 ++-- src/kernel_internals/runtime/fc_config.mli | 2 +- src/kernel_internals/runtime/special_hooks.ml | 4 ++-- src/kernel_internals/typing/mergecil.ml | 2 +- src/kernel_services/ast_queries/file.mli | 2 +- .../plugin_entry_points/kernel.ml | 8 +++---- src/plugins/e-acsl/doc/userman/provides.tex | 6 ++--- src/plugins/e-acsl/man/e-acsl-gcc.sh.1 | 6 ++--- src/plugins/e-acsl/scripts/e-acsl-gcc.sh | 2 +- 20 files changed, 59 insertions(+), 59 deletions(-) diff --git a/doc/aorai/SrcSchemas/GeneralView.fig b/doc/aorai/SrcSchemas/GeneralView.fig index e76fbfcf399..ce725c75e54 100644 --- a/doc/aorai/SrcSchemas/GeneralView.fig +++ b/doc/aorai/SrcSchemas/GeneralView.fig @@ -66,7 +66,7 @@ Single 4 0 0 50 -1 3 12 0.0000 0 135 315 1890 6255 LTL\001 4 0 0 50 -1 2 12 0.0000 0 180 405 8865 6390 Why\001 4 0 0 50 -1 3 12 0.0000 0 180 900 1305 5220 C Program\001 -4 0 0 50 -1 2 12 0.0000 0 180 1995 2745 5220 Frama-C pre-processor\001 +4 0 0 50 -1 2 12 0.0000 0 180 1995 2745 5220 Frama-C preprocessor\001 4 0 0 50 -1 1 12 0.0000 0 180 855 3015 6210 Simplified\001 4 0 0 50 -1 1 12 0.0000 0 135 360 3240 6435 LTL\001 4 0 0 50 -1 1 12 0.0000 0 135 1290 6210 6300 B\374chi automata\001 diff --git a/doc/aorai/main.tex b/doc/aorai/main.tex index 43ed2deea1d..2894f0544c3 100644 --- a/doc/aorai/main.tex +++ b/doc/aorai/main.tex @@ -1084,7 +1084,7 @@ current active states, since it knows each previous active states. \node[yshift=-6em] (prop) at (c) {\it Property}; \node[yshift=-3em] (ya) at (prop) {\it Ya automaton}; - \node[draw,xshift=10ex,anchor=west,align=center,font=\bfseries] (fc) at (c.east) {Frama-C\\pre-processor}; + \node[draw,xshift=10ex,anchor=west,align=center,font=\bfseries] (fc) at (c.east) {Frama-C\\preprocessor}; \node[draw,xshift=10ex,anchor=west,align=center,font=\bfseries] (annot) at (fc.east) {Annotations\\calculus}; \node[ellipse,draw,yshift=-6em,align=center] (buchi) at (annot) {Büchi\\automaton}; diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex index 5e2815b5d6c..c2945e32fa6 100644 --- a/doc/developer/advance.tex +++ b/doc/developer/advance.tex @@ -3172,7 +3172,7 @@ over which the analyses are performed. Customization of the front-end of \item\textbf{Parsing:} this stage takes care of converting an individual source file into a parsed AST (a.k.a Cabs, which differs from the type-checked AST on which most analyses operate). By default, source files are treated as C files, -possibly needing a pre-processing phase. It is possible to tell Frama-C to use +possibly needing a preprocessing phase. It is possible to tell Frama-C to use another parser for files ending with a given suffix by registering this parser with the \texttt{File.new\_file\_type}\scodeidxdef{File}{new\_file\_type} function. Suffixes \texttt{.h}, \texttt{.i}, \texttt{.c} and \texttt{.ci} @@ -3286,7 +3286,7 @@ We present below a thorough description of each field. Note that some compiler extensions, such as attributes, are always enabled. \item[\texttt{cpp\_arch\_flags}]: list of arguments used by the compiler to select the corresponding architecture, e.g. \verb+["-m32"]+ for a 32-bit - machdep. Older versions (up to 26.x - Iron) of \framac did pass these flags to the pre-processor, + machdep. Older versions (up to 26.x - Iron) of \framac did pass these flags to the preprocessor, in order for it to define a set of built-in macros related to said architecture. Current versions do not use this field, and rely on \texttt{\texttt{custom\_defs}} containing the appropriate definitions. diff --git a/doc/eva/main.tex b/doc/eva/main.tex index 69d339635e2..db5e6118833 100644 --- a/doc/eva/main.tex +++ b/doc/eva/main.tex @@ -369,12 +369,12 @@ frama-c -eva main_1.c > log Frama-C has its own model of the target platform (the default target is a little-endian 64-bit platform). It also uses the host system's preprocessor. If you want to do the analysis for a different platform than the host platform, -you need to provide Frama-C with a way to pre-process the files as they +you need to provide Frama-C with a way to preprocess the files as they would be during an actual compilation. There are analyses where the influence of host platform parameters is not noticeable. The analysis we are embarking on is not one of them. -If you pre-process the Skein source code with a 32-bit compiler and +If you preprocess the Skein source code with a 32-bit compiler and then analyze it with Frama-C targeting its default 64-bit platform, the analysis will be meaningless and you won't be able to make sense of this tutorial. @@ -2964,12 +2964,12 @@ $\dots$ The analyzed files should be syntactically correct C. The files that do not use the {\tt .i} extension are automatically -pre-processed. The preprocessing command used by default is +preprocessed. The preprocessing command used by default is \lstinline|gcc -C -E -I.|, but another preprocessor may be employed. It is possible that files without a {\tt .c} extension fail to pass this stage. It is notably the case with \lstinline|gcc|, -to which the option \lstinline|-x c| should be passed in order to pre-process +to which the option \lstinline|-x c| should be passed in order to preprocess C files that do not have a \lstinline|.c| extension. \goodbreak diff --git a/doc/rte/rte.tex b/doc/rte/rte.tex index 2dde9b169e3..137149415ab 100644 --- a/doc/rte/rte.tex +++ b/doc/rte/rte.tex @@ -223,7 +223,7 @@ type & size & representable interval \\ \medskip Frama-C annotations added by plug-ins such as \rte{} may not contain macros -since pre-processing is supposed to take place beforehand (user annotations at +since preprocessing is supposed to take place beforehand (user annotations at the source level can be taken into account by using the \lstinline|-pp-annot| option). As a consequence, annotations are displayed with big constants such as those appearing in this table. diff --git a/doc/userman/user-changes.tex b/doc/userman/user-changes.tex index f5f6cc841c1..6f613040deb 100644 --- a/doc/userman/user-changes.tex +++ b/doc/userman/user-changes.tex @@ -162,7 +162,7 @@ predefined by \FramaC (Section~\ref{sec:predefined-macros}). \begin{itemize} \item \textbf{Normalizing the Source Code:} new options \texttt{-initialized-padding-locals} and \texttt{-simplify-trivial-loops}. -\item \textbf{Pre-processing the Source Files:} new options +\item \textbf{Preprocessing the Source Files:} new options \texttt{-cpp-gnu-like} and \texttt{-frama-c-stdlib}. \item \textbf{Customizing Analyzers:} new options \texttt{-add-symbolic-path} and \texttt{-permissive}. diff --git a/doc/userman/user-intro.tex b/doc/userman/user-intro.tex index b89a4fd4268..ec0b85002ea 100644 --- a/doc/userman/user-intro.tex +++ b/doc/userman/user-intro.tex @@ -44,7 +44,7 @@ The remainder of this manual is organized in several chapters. \item[Chapter~\ref{user-plugins}] explains the basics of plug-in categories, installation, and usage. \item[Chapter~\ref{user-sources}] presents the options of the source code - pre-processor. + preprocessor. \item[Chapter~\ref{user-analysis}] gives some general options for parameterizing analyzers. \item[Chapter~\ref{user-properties}] touches on the topic of code properties, diff --git a/doc/userman/user-start.tex b/doc/userman/user-start.tex index 5fd63f1898a..b0dec842511 100644 --- a/doc/userman/user-start.tex +++ b/doc/userman/user-start.tex @@ -35,9 +35,9 @@ file of the source distribution. The main components necessary for compiling and running \FramaC are described below. \begin{description} -\item[A \C pre-processor]\index{C pre-processor} is required for \emph{using} - \FramaC on \C files. If you do not have any \C pre-processor, - you can only run \FramaC on already pre-processed \texttt{.i} files. +\item[A \C preprocessor]\index{C preprocessor} is required for \emph{using} + \FramaC on \C files. If you do not have any \C preprocessor, + you can only run \FramaC on already preprocessed \texttt{.i} files. \item[A \C compiler]\index{C compiler} is required to compile the \FramaC kernel. \item[A \tool{Unix}-like compilation environment] with at least the tool diff --git a/man/frama-c.1 b/man/frama-c.1 index 1864494be98..f292872c684 100644 --- a/man/frama-c.1 +++ b/man/frama-c.1 @@ -50,10 +50,10 @@ It features the same options as the command-line version. It also features the same options as the command-line version. .PP By default, Frama-C recognizes \f[I].c\f[R] files as C files needing -pre-processing and \f[I].i\f[R] files as C files having been already -pre-processed. +preprocessing and \f[I].i\f[R] files as C files having been already +preprocessed. Some plugins may extend the list of recognized files. -Pre-processing can be customized through the \f[B]-cpp-command\f[R] and +Preprocessing can be customized through the \f[B]-cpp-command\f[R] and \f[B]-cpp-extra-args\f[R] options. .SH OPTIONS .SS Syntax @@ -129,7 +129,7 @@ Defaults to yes. [-no]-annot reads ACSL annotations. This is the default. -Annotations are pre-processed by default. +Annotations are preprocessed by default. Use -no-pp-annot if you don\[cq]t want to expand macros in annotations. .TP [-no]-ast-diff @@ -188,7 +188,7 @@ code are still fatal, though). instead. .TP -cpp-command \f[I]cmd\f[R] -uses \f[I]cmd\f[R] as the command to pre-process C files. +uses \f[I]cmd\f[R] as the command to preprocess C files. Defaults to the \f[B]CPP\f[R] environment variable or to .RS .PP @@ -208,13 +208,13 @@ Note that this option is often better replaced by \f[B]-cpp-extra-args\f[R]. .TP -cpp-extra-args \f[I]args\f[R] -gives additional arguments to the pre-processor. -Pre-processing annotations is done in two separate pre-processing +gives additional arguments to the preprocessor. +Preprocessing annotations is done in two separate preprocessing stages. The first one is a normal pass on the C code which retains macro definitions. These are then used in the second pass during which annotations are -pre-processed. +preprocessed. \f[I]args\f[R] are used only for the first pass, so that arguments that should not be used twice (such as additional include directives or macro definitions) must thus go there instead of \f[B]-cpp-command\f[R]. @@ -406,10 +406,10 @@ When this option is on, a message is printed each time this occurs. Defaults to no. .TP [-no]-pp-annot -pre-processes annotations. +preprocesses annotations. This is currently only possible when using gcc (or GNU cpp) -pre-processor. -The default is to pre-process annotations when the default pre-processor +preprocessor. +The default is to preprocess annotations when the default preprocessor is identified as GNU or GNU-like. See also \f[B]-cpp-frama-c-compliant\f[R]. .TP diff --git a/man/frama-c.1.md b/man/frama-c.1.md index 9c1876b46f6..e8c36a9d6e5 100644 --- a/man/frama-c.1.md +++ b/man/frama-c.1.md @@ -47,10 +47,10 @@ It features the same options as the command-line version. **ivette** is a new, Electron-based graphical user interface for **frama-c**. It also features the same options as the command-line version. -By default, Frama-C recognizes *.c* files as C files needing pre-processing -and *.i* files as C files having been already pre-processed. +By default, Frama-C recognizes *.c* files as C files needing preprocessing +and *.i* files as C files having been already preprocessed. Some plugins may extend the list of recognized files. -Pre-processing can be customized through the **-cpp-command** and +Preprocessing can be customized through the **-cpp-command** and **-cpp-extra-args** options. # OPTIONS @@ -116,7 +116,7 @@ Otherwise, normalization uses labels and gotos. Bigger blocks and blocks with non-trivial control flow are never duplicated. Defaults to yes. [-no]-annot -: reads ACSL annotations. This is the default. Annotations are pre-processed +: reads ACSL annotations. This is the default. Annotations are preprocessed by default. Use -no-pp-annot if you don't want to expand macros in annotations. [-no]-ast-diff @@ -164,7 +164,7 @@ typeâ€checking will continue (errors in C code are still fatal, though). \ **Deprecated**: use **-kernel-warn-key annot-error** instead. -cpp-command *cmd* -: uses *cmd* as the command to pre-process C files. +: uses *cmd* as the command to preprocess C files. Defaults to the **CPP** environment variable or to > gcc -C -E -I. @@ -178,11 +178,11 @@ position of *<source file>* and *<preprocessed file>* respectively. Note that this option is often better replaced by **-cpp-extra-args**. -cpp-extra-args *args* -: gives additional arguments to the pre-processor. -Pre-processing annotations is done in two separate pre-processing stages. +: gives additional arguments to the preprocessor. +Preprocessing annotations is done in two separate preprocessing stages. The first one is a normal pass on the C code which retains macro definitions. These are then used in the second pass during which annotations are -pre-processed. *args* are used only for the first pass, so that arguments that +preprocessed. *args* are used only for the first pass, so that arguments that should not be used twice (such as additional include directives or macro definitions) must thus go there instead of **-cpp-command**. @@ -343,9 +343,9 @@ and a formal parameter). When this option is on, a message is printed each time this occurs. Defaults to no. [-no]-pp-annot -: pre-processes annotations. This is currently only possible when using gcc -(or GNU cpp) pre-processor. The default is to pre-process annotations when the -default pre-processor is identified as GNU or GNU-like. +: preprocesses annotations. This is currently only possible when using gcc +(or GNU cpp) preprocessor. The default is to preprocess annotations when the +default preprocessor is identified as GNU or GNU-like. See also **-cpp-frama-c-compliant**. [-no]-print diff --git a/src/kernel_internals/parsing/logic_preprocess.mli b/src/kernel_internals/parsing/logic_preprocess.mli index 22be86b519c..9bd5ba2de70 100644 --- a/src/kernel_internals/parsing/logic_preprocess.mli +++ b/src/kernel_internals/parsing/logic_preprocess.mli @@ -22,15 +22,15 @@ (* *) (**************************************************************************) -(** adds another pre-processing step in order to expand macros in +(** adds another preprocessing step in order to expand macros in annotations. *) (** [file suffix cpp file] takes the file to preprocess, - and the pre-processing directive, and returns the name of the file - containing the completely pre-processed source. suffix will be appended - to the name of intermediate files generated for pre-processing annotations - (gcc pre-processing differs between .c and .cxx files) + and the preprocessing directive, and returns the name of the file + containing the completely preprocessed source. suffix will be appended + to the name of intermediate files generated for preprocessing annotations + (gcc preprocessing differs between .c and .cxx files) @raises Sys_error if the file cannot be opened. *) diff --git a/src/kernel_internals/parsing/logic_preprocess.mll b/src/kernel_internals/parsing/logic_preprocess.mll index 02ed925af56..f973492af2b 100644 --- a/src/kernel_internals/parsing/logic_preprocess.mll +++ b/src/kernel_internals/parsing/logic_preprocess.mll @@ -147,7 +147,7 @@ with_nl, decode_utf8 @@ replace_backslash content with End_of_file -> Kernel.fatal - "too few annotations in result file while pre-processing annotations" + "too few annotations in result file while preprocessing annotations" let output_result outfile preprocessed content = let rec aux = function @@ -173,7 +173,7 @@ try Extlib.temp_file_cleanup_at_exit ~debug "ppannot" suffix with Extlib.Temp_file_error s -> Kernel.abort - "Could not open temporary file for logic pre-processing: %s" s + "Could not open temporary file for logic preprocessing: %s" s in let ppfile = open_out ppname in Buffer.output_buffer ppfile preprocess_buffer; diff --git a/src/kernel_internals/runtime/fc_config.mli b/src/kernel_internals/runtime/fc_config.mli index 1af06ba4e25..a9ec0d19da2 100644 --- a/src/kernel_internals/runtime/fc_config.mli +++ b/src/kernel_internals/runtime/fc_config.mli @@ -94,7 +94,7 @@ val using_default_cpp: bool val preprocessor_is_gnu_like: bool (** whether the default preprocessor accepts the same options as gcc (i.e. is either gcc or clang), when this is the case, the default - command line for pre-processing contains more options. + command line for preprocessing contains more options. @since Sodium-20150201 *) diff --git a/src/kernel_internals/runtime/special_hooks.ml b/src/kernel_internals/runtime/special_hooks.ml index bef0ed22ed0..96deb0afdae 100644 --- a/src/kernel_internals/runtime/special_hooks.ml +++ b/src/kernel_internals/runtime/special_hooks.ml @@ -39,10 +39,10 @@ let print_config () = (String.concat ":" (Filepath.Normalized.to_string_list Fc_config.libdirs)) (fun fmt -> if Fc_config.preprocessor = "" then - Format.fprintf fmt "@\nWarning: no default pre-processor" + Format.fprintf fmt "@\nWarning: no default preprocessor" else if not Fc_config.preprocessor_keep_comments then Format.fprintf fmt - "@\nWarning: default pre-processor is not able to keep comments \ + "@\nWarning: default preprocessor is not able to keep comments \ (hence ACSL annotations) in its output") ; ); diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml index cdccc797c7e..f4515f22aa9 100644 --- a/src/kernel_internals/typing/mergecil.ml +++ b/src/kernel_internals/typing/mergecil.ml @@ -1549,7 +1549,7 @@ let matchModelField (* First pass might decide to ignore some globals that are not used in their own translation unit and have type incompatible with the one associated - to the symbol names in already pre-processed files. We store + to the symbol names in already preprocessed files. We store the corresponding varinfos here and ensure that we do not attempt to extract some information (notably function contract or function definition) from them in pass 2. diff --git a/src/kernel_services/ast_queries/file.mli b/src/kernel_services/ast_queries/file.mli index d3d89a240a9..f30c12ffde2 100644 --- a/src/kernel_services/ast_queries/file.mli +++ b/src/kernel_services/ast_queries/file.mli @@ -39,7 +39,7 @@ type file = - cpp_opt_kind: whether the preprocessor supports GNU options such as -I/-D. *) | NoCPP of Filepath.Normalized.t - (** Already pre-processed file [.i] *) + (** Already preprocessed file [.i] *) | External of Filepath.Normalized.t * string (** file that can be translated into a Cil AST through an external function, together with the recognized suffix. *) diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml index eae3f26f41a..b2d28443a78 100644 --- a/src/kernel_services/plugin_entry_points/kernel.ml +++ b/src/kernel_services/plugin_entry_points/kernel.ml @@ -1012,8 +1012,8 @@ module PreprocessAnnot = let module_name = "PreprocessAnnot" let option_name = "-pp-annot" let help = - "pre-process annotations (if they are read). Set by default if \ - the pre-processor is GNU-like (see option -cpp-frama-c-compliant)" + "preprocess annotations (if they are read). Set by default if \ + the preprocessor is GNU-like (see option -cpp-frama-c-compliant)" end) let () = Parameter_customize.set_group parsing @@ -1068,9 +1068,9 @@ module CppGnuLike = let module_name = "CppGnuLike" let option_name = "-cpp-frama-c-compliant" let help = - "indicates that a custom pre-processor (see option -cpp-command) \ + "indicates that a custom preprocessor (see option -cpp-command) \ accepts the same set of options as GNU cpp. Set it to false if you \ - have pre-processing issues with a custom pre-processor." + have preprocessing issues with a custom preprocessor." end) let () = Parameter_customize.set_group parsing diff --git a/src/plugins/e-acsl/doc/userman/provides.tex b/src/plugins/e-acsl/doc/userman/provides.tex index 7e5b59bf568..5080d6b62c2 100644 --- a/src/plugins/e-acsl/doc/userman/provides.tex +++ b/src/plugins/e-acsl/doc/userman/provides.tex @@ -50,7 +50,7 @@ to the \framac command line: [e-acsl] translation done in project "e-acsl". \end{shell} -Even though \texttt{first.i} has already been pre-processed, \eacsl first asks +Even though \texttt{first.i} has already been preprocessed, \eacsl first asks the \framac kernel to process and combine it against several header files provided by the \eacsl plug-in. Further \eacsl translates the annotated code into a new \framac project named \texttt{e-acsl}\footnote{The notion of @@ -233,7 +233,7 @@ respectively, for instance as follows: Runs of \framac and \gcc issued by \eacslgcc can further be customized by using additional flags. \framac flags can be passed using the \shortopt{F} option, while \shortopt{e} and \shortopt{l} options allow for passing additional -pre-processor and linker flags during \gcc invocations. For example, command +preprocessor and linker flags during \gcc invocations. For example, command \begin{frama-c-commands} \$ e-acsl-gcc.sh -c -F"-unicode" -e"-I/bar -I/baz" foo.c @@ -246,7 +246,7 @@ are output using the UTF-8 character set. Further, during the compilation of It is worth mentioning that \eacslgcc implements several convenience flags for setting some of the \framac options. For instance, \shortopt{E} can be used to -pass additional arguments to the \framac pre-processor (see +pass additional arguments to the \framac preprocessor (see Section~\ref{sec:eacsl-gcc:doc}). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 index 314e63b51a6..068cc396f4b 100644 --- a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 +++ b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 @@ -94,7 +94,7 @@ Unless specified, the executable is named as inidicated by the \fB--oexec\fP opt run input source files through \fBFrama-C\fP without \fBE-ACSL\fP instrumentations. .TP .B -E, --extra-cpp-args=\fI<FLAGS> -pass additional arguments to the \fBFrama-C\fP pre-processor. +pass additional arguments to the \fBFrama-C\fP preprocessor. .TP .B -L, --frama-c-stdlib use the \fBFrama-C\fP standard library instead of a system-wide one. @@ -137,8 +137,8 @@ compiler. pass the specified flags to the linker. .TP .B -e, --cpp-flags=\fI<FLAGS> -pass the specified flags to the pre-processor at compile-time. -For instrumentation-time pre-processor flags see \fB--extra-cpp-args\fP option. +pass the specified flags to the preprocessor at compile-time. +For instrumentation-time preprocessor flags see \fB--extra-cpp-args\fP option. .TP .B -q, --quiet suppress any output except for errors and warnings. diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh index 67d55a79118..b62985f0e54 100755 --- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh +++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh @@ -548,7 +548,7 @@ do OPTION_LDFLAGS="$OPTION_LDFLAGS $1" shift; ;; - # Additional flags passed to the pre-processor (compile-time) + # Additional flags passed to the preprocessor (compile-time) --cpp-flags|-e) shift; OPTION_CPPFLAGS="$OPTION_CPPFLAGS $1" -- GitLab