diff --git a/doc/userman/user-sources.tex b/doc/userman/user-sources.tex index 0c352fbc84c508b0610191cc18168a9fa79571a5..8bf11cb8b715d5bf766ce1ef1da13041d1c356b7 100644 --- a/doc/userman/user-sources.tex +++ b/doc/userman/user-sources.tex @@ -15,25 +15,36 @@ pre-processes the other files with the following command. \end{shell} The option \optiondef{-}{cpp-command} may be used to change -the default pre-processing command. If patterns \texttt{\%1} and \texttt{\%2} -do not appear in the provided command, the pre-processor is invoked in the +the default pre-processing command. Placeholders can be used for advanced +commands. If no placeholders are used, the pre-processor is invoked in the following way. \begin{commands} -\texttt{<cmd> -o <output file> <input file>} +\texttt{<cmd> <args> -o <output file> <input file>} \end{commands} In this command, \texttt{<output file>} is chosen by \FramaC while \texttt{<input file>} is one of the filenames provided by the user. -It is also possible to -use the patterns \texttt{\%1} and \texttt{\%2} in the command as place-holders -for the input files and the output file respectively. Here are some examples -for using this option. + +For commands which do not follow this pattern, it is also possible to use +the following patterns: + +\begin{tabular}{|l|l|} +\hline +\texttt{\%input}, \texttt{\%i} or \texttt{\%1} & Input file \\ +\hline +\texttt{\%output}, \texttt{\%o} or \texttt{\%2} & Output file \\ +\hline +\texttt{\%args} & Additional arguments (see \texttt{-cpp-extra-args} below)\\ +\hline +\end{tabular} + +Here are some examples for using this option. \begin{shell} \$ frama-c -cpp-command 'gcc -C -E -I. -x c' file1.src file2.i -\$ frama-c -cpp-command 'gcc -C -E -I. -o %2 %1' file1.c file2.i -\$ frama-c -cpp-command 'cp %1 %2' file1.c file2.i -\$ frama-c -cpp-command 'cat %1 > %2' file1.c file2.i -\$ frama-c -cpp-command 'CL.exe /C /E %1 > %2' file1.c file2.i +\$ frama-c -cpp-command 'gcc -C -E -I. %args -o %o %i' file1.c file2.i +\$ frama-c -cpp-command 'cp %i %o' file1.c file2.i +\$ frama-c -cpp-command 'cat %i > %o' file1.c file2.i +\$ frama-c -cpp-command 'CL.exe /C /E %args %i > %o' file1.c file2.i \end{shell} If you use the above option, you may use the option \optiondef{-}{cpp-frama-c-compliant}