Commit | Line | Data |
---|---|---|
faf9a90c C |
1 | \section{Introduction} |
2 | ||
3 | This document describes the options provided by Coccinelle. The options | |
4 | have an impact on various phases of the semantic patch application | |
5 | process. These are: | |
6 | ||
7 | \begin{enumerate} | |
8 | \item Selecting and parsing the semantic patch. | |
9 | \item Selecting and parsing the C code. | |
10 | \item Application of the semantic patch to the C code. | |
11 | \item Transformation. | |
12 | \item Generation of the result. | |
13 | \end{enumerate} | |
14 | ||
15 | \noindent | |
16 | One can either initiate the complete process from step 1, or | |
17 | to perform step 1 or step 2 individually. | |
18 | ||
19 | Coccinelle has quite a lot of options. The most common usages are as | |
20 | follows, for a semantic match {\tt foo.cocci}, a C file {\tt foo.c}, and a | |
21 | directory {\tt foodir}: | |
22 | ||
23 | \begin{itemize} | |
17ba0788 | 24 | \item {\tt spatch --parse-cocci foo.cocci}: Check that the semantic patch |
faf9a90c | 25 | is syntactically correct. |
17ba0788 | 26 | \item {\tt spatch --parse-c foo.c}: Check that the C file |
faf9a90c C |
27 | is syntactically correct. The Coccinelle C parser tries to recover |
28 | during the parsing process, so if one function does not parse, it will | |
29 | start up again with the next one. Thus, a parse error is often not a | |
30 | cause for concern, unless it occurs in a function that is relevant to the | |
31 | semantic patch. | |
17ba0788 | 32 | \item {\tt spatch --sp-file foo.cocci foo.c}: Apply the semantic patch {\tt |
faf9a90c | 33 | foo.cocci} to the file {\tt foo.c} and print out any transformations as a |
17ba0788 C |
34 | diff. {\tt --sp-file} is optional in this and the following cases. |
35 | \item {\tt spatch --sp-file foo.cocci foo.c --debug}: The same as the | |
faf9a90c | 36 | previous case, but print out some information about the matching process. |
17ba0788 | 37 | \item {\tt spatch --sp-file foo.cocci --dir foodir}: Apply the semantic |
faf9a90c | 38 | patch {\tt foo.cocci} to all of the C files in the directory {\tt foodir}. |
17ba0788 | 39 | \item {\tt spatch --sp-file foo.cocci --dir foodir --include-headers}: Apply |
faf9a90c C |
40 | the semantic patch {\tt foo.cocci} to all of the C files and header files |
41 | in the directory {\tt foodir}. | |
42 | \end{itemize} | |
43 | ||
44 | In the rest of this document, the options are annotated as follows: | |
45 | \begin{itemize} | |
46 | \item \FilledBigDiamondshape: a basic option, that is most likely of | |
47 | interest to all users. | |
48 | \item \BigLowerDiamond: an option that is frequently used, often for better | |
49 | understanding the effect of a semantic patch. | |
50 | \item \BigDiamondshape: an option that is likely to be rarely used, but | |
51 | whose effect is still comprehensible to a user. | |
52 | \item An option with no annotation is likely of interest only to | |
53 | developers. | |
54 | \end{itemize} | |
55 | ||
56 | \section{Selecting and parsing the semantic patch} | |
57 | ||
58 | \subsection{Standalone options} | |
59 | ||
17ba0788 | 60 | \normal{--parse-cocci $\langle$file$\rangle$}{ Parse a semantic |
faf9a90c C |
61 | patch file and print out some information about it.} |
62 | ||
63 | \subsection{The semantic patch} | |
64 | ||
17ba0788 C |
65 | \minimum{--sp-file $\langle$file$\rangle$, -c $\langle$file$\rangle$, |
66 | -cocci-file $\langle$file$\rangle$}{ Specify the name of the file | |
faf9a90c | 67 | containing the semantic patch. The file name should end in {\tt .cocci}. |
993936c0 C |
68 | All three options do the same thing. These options are optional. If they |
69 | are not used, the single file whose name ends in \texttt{.cocci} is | |
70 | assoumed to be the name of the file containing the semantic patch.} | |
71 | ||
17ba0788 | 72 | \rare{--sp ``semantic patch string''}{Specify a semantic match as a |
993936c0 C |
73 | command-line argument. See the section ``Command-line semantic match'' |
74 | in the manual.} | |
faf9a90c C |
75 | |
76 | \subsection{Isomorphisms} | |
77 | ||
17ba0788 | 78 | \rare{--iso, --iso-file}{ Specify a file containing isomorphisms to be used in |
faf9a90c C |
79 | place of the standard one. Normally one should use the {\tt using} |
80 | construct within a semantic patch to specify isomorphisms to be used {\em | |
81 | in addition to} the standard ones.} | |
82 | ||
17ba0788 | 83 | \rare{--iso-limit $\langle$int$\rangle$} Limit the depth of application of |
b1b2de81 C |
84 | isomorphisms to the specified integer. |
85 | ||
17ba0788 | 86 | \rare{--no-iso-limit} Put no limit on the number of times that |
b1b2de81 C |
87 | isomorphisms can be applied. This is the default. |
88 | ||
17ba0788 | 89 | \rare{--disable-iso}{Disable a specific isomorphism from the command line. |
413ffc02 C |
90 | This option can be specified multiple times.} |
91 | ||
17ba0788 | 92 | \developer{--track-iso}{ Gather information about isomorphism usage.} |
faf9a90c | 93 | |
17ba0788 | 94 | \developer{--profile-iso}{ Gather information about the time required for |
faf9a90c C |
95 | isomorphism expansion.} |
96 | ||
97 | \subsection{Display options} | |
98 | ||
17ba0788 | 99 | \rare{--show-cocci}{Show the semantic patch that is being processed before |
faf9a90c C |
100 | expanding isomorphisms.} |
101 | ||
17ba0788 | 102 | \rare{--show-SP}{Show the semantic patch that is being processed after |
faf9a90c C |
103 | expanding isomorphisms.} |
104 | ||
17ba0788 | 105 | \rare{--show-ctl-text}{ Show the representation |
faf9a90c C |
106 | of the semantic patch in CTL.} |
107 | ||
17ba0788 | 108 | \rare{--ctl-inline-let}{ Sometimes {\tt let} is used to name |
faf9a90c C |
109 | intermediate terms CTL representation. This option causes the let-bound |
110 | terms to be inlined at the point of their reference. | |
17ba0788 | 111 | This option implicitly sets {\bf --show-ctl-text}.} |
faf9a90c | 112 | |
17ba0788 | 113 | \rare{--ctl-show-mcodekind}{ Show |
faf9a90c | 114 | transformation information within the CTL representation |
17ba0788 | 115 | of the semantic patch. This option implicitly sets {\bf --show-ctl-text}.} |
faf9a90c | 116 | |
17ba0788 | 117 | \rare{--show-ctl-tex}{ Create a LaTeX files showing the representation |
faf9a90c C |
118 | of the semantic patch in CTL.} |
119 | ||
120 | \section{Selecting and parsing the C files} | |
121 | ||
122 | \subsection{Standalone options} | |
123 | ||
17ba0788 | 124 | \normal{--parse-c $\langle$file/dir$\rangle$}{ Parse a {\tt .c} file or all |
faf9a90c C |
125 | of the {\tt .c} files in a directory. This generates information about |
126 | any parse errors encountered.} | |
127 | ||
17ba0788 | 128 | \normal{--parse-h $\langle$file/dir$\rangle$}{ Parse a {\tt .h} file or all |
faf9a90c C |
129 | of the {\tt .h} files in a directory. This generates information about |
130 | any parse errors encountered.} | |
131 | ||
17ba0788 | 132 | \normal{--parse-ch $\langle$file/dir$\rangle$}{ Parse a {\tt .c} or {\tt |
faf9a90c C |
133 | .h} file or all of the {\tt .c} or {\tt .h} files in a directory. This |
134 | generates information about any parse errors encountered.} | |
135 | ||
17ba0788 | 136 | \normal{--control-flow $\langle$file$\rangle$, --control-flow |
faf9a90c C |
137 | $\langle$file$\rangle$:$\langle$function$\rangle$}{ Print a control-flow |
138 | graph for all of the functions in a file or for a specific function in a | |
139 | file. This requires {\tt dot} (http://www.graphviz.org/) and {\tt gv}.} | |
140 | ||
17ba0788 C |
141 | \rare{--control-flow-to-file $\langle$file$\rangle$, |
142 | --control-flow-to-file | |
143 | $\langle$file$\rangle$:$\langle$function$\rangle$}{ Like --control-flow | |
4dfbc1c2 C |
144 | but just puts the dot output in a file in the {\em current} directory. |
145 | For PATH/file.c, this produces file:xxx.dot for each (selected) function | |
146 | xxx in PATH/file.c.} | |
147 | ||
17ba0788 | 148 | \rare{--type-c $\langle$file$\rangle$}{ Parse a C file and pretty-print a |
faf9a90c C |
149 | version including type information.} |
150 | ||
17ba0788 | 151 | \developer{--tokens-c $\langle$file$\rangle$}{Prints the tokens in a C |
faf9a90c C |
152 | file.} |
153 | ||
17ba0788 | 154 | \developer{--parse-unparse $\langle$file$\rangle$}{Parse and then reconstruct |
faf9a90c C |
155 | a C file.} |
156 | ||
17ba0788 C |
157 | \developer{--compare-c $\langle$file$\rangle$ $\langle$file$\rangle$, |
158 | --compare-c-hardcoded}{Compares one C file to another, or compare the | |
faf9a90c C |
159 | file tests/compare1.c to the file tests/compare2.c.} |
160 | ||
17ba0788 | 161 | \developer{--test-cfg-ifdef $\langle$file$\rangle$}{Do some special |
faf9a90c C |
162 | processing of \#ifdef and display the resulting control-flow graph. This |
163 | requires {\tt dot} and {\tt gv}.} | |
164 | ||
17ba0788 C |
165 | \developer{--test-attributes $\langle$file$\rangle$, |
166 | --test-cpp $\langle$file$\rangle$}{ | |
faf9a90c C |
167 | Test the parsing of cpp code and attributes, respectively.} |
168 | ||
169 | \subsection{Selecting C files} | |
170 | ||
708f4980 C |
171 | An argument that ends in {\tt .c} is assumed to be a C file to process. |
172 | Normally, only one C file or one directory is specified. If multiple C | |
173 | files are specified, they are treated in parallel, {\em i.e.}, the first | |
174 | semantic patch rule is applied to all functions in all files, then the | |
175 | second semantic patch rule is applied to all functions in all files, etc. | |
176 | If a directory is specified then no files may be specified and only the | |
faf9a90c C |
177 | rightmost directory specified is used. |
178 | ||
17ba0788 | 179 | \normal{--include-headers}{ This option causes header files to be processed |
faf9a90c | 180 | independently. This option only makes sense if a directory is specified |
17ba0788 | 181 | using {\bf --dir}.} |
faf9a90c | 182 | |
17ba0788 | 183 | \normal{--use-glimpse}{ Use a glimpse index to select the files to which |
faf9a90c C |
184 | a semantic patch may be relevant. This option requires that a directory is |
185 | specified. The index may be created using the script {\tt | |
17ba0788 C |
186 | coccinelle/scripts/ glimpseindex-cocci.sh}. Glimpse is available at |
187 | http://webglimpse.net/. In conjunction with the option {\bf --patch-cocci} | |
faf9a90c C |
188 | this option prints the regular expression that will be passed to glimpse.} |
189 | ||
17ba0788 | 190 | \normal{--use-idutils}{ Use an id-utils index created using lid to select |
1eddfd50 C |
191 | the files to which a semantic patch may be relevant. This option |
192 | requires that a directory is specified. The index may be created using | |
17ba0788 C |
193 | the script {\tt coccinelle/scripts/ idindex-cocci.sh}. In conjunction |
194 | with the option {\bf --patch-cocci} this option prints the regular | |
1eddfd50 C |
195 | expression that will be passed to glimpse.} |
196 | ||
17ba0788 | 197 | \rare{--dir}{ Specify a directory containing C files to process. A trailing |
c3e37e97 C |
198 | {\tt /} is permitted on the directory name and has no impact on the |
199 | result. By default, the include path will be set to the ``include'' | |
200 | subdirectory of this directory. A different include path can be | |
17ba0788 | 201 | specified using the option {\bf -I}. {\bf --dir} only considers the |
c3e37e97 C |
202 | rightmost directory in the argument list. This behavior is convenient |
203 | for creating a script that always works on a single directory, but allows | |
204 | the user of the script to override the provided directory with another | |
205 | one. Spatch collects the files in the directory using {\tt find} and | |
206 | does not follow symbolic links.} | |
708f4980 | 207 | |
17ba0788 | 208 | \developer{--kbuild-info $\langle$file$\rangle$}{ The specified file |
faf9a90c C |
209 | contains information about which sets of files should be considered in |
210 | parallel.} | |
211 | ||
17ba0788 | 212 | \developer{--disable-worth-trying-opt}{Normally, a C file is only |
faf9a90c C |
213 | processed if it contains some keywords that have been determined to be |
214 | essential for the semantic patch to match somewhere in the file. This | |
215 | option disables this optimization and tries the semantic patch on all files.} | |
216 | ||
17ba0788 | 217 | \developer{--test $\langle$file$\rangle$}{ A shortcut for running Coccinelle |
faf9a90c C |
218 | on the semantic patch ``file{\tt{.cocci}}'' and the C file ``file{\tt{.c}}''.} |
219 | ||
17ba0788 | 220 | \developer{--testall}{A shortcut for running Coccinelle on all files in a |
faf9a90c C |
221 | subdirectory {\tt tests} such that there are all of a {\tt .cocci} file, a {\tt |
222 | .c} file, and a {\tt .res} file, where the {\tt .res} contains the | |
223 | expected result.} | |
224 | ||
17ba0788 | 225 | \developer{--test-okfailed, --test-regression-okfailed} Other options for |
faf9a90c C |
226 | keeping track of tests that have succeeded and failed. |
227 | ||
17ba0788 | 228 | \developer{--compare-with-expected}{Compare the result of applying |
faf9a90c C |
229 | Coccinelle to file{\tt{.c}} to the file file{\tt{.res}} representing the |
230 | expected result.} | |
231 | ||
17ba0788 | 232 | \developer{--expected-score-file $\langle$file$\rangle$}{ |
708f4980 C |
233 | which score file to compare with in the testall run} |
234 | ||
faf9a90c C |
235 | \subsection{Parsing C files} |
236 | ||
17ba0788 | 237 | \rare{--show-c}{Show the C code that is being processed.} |
faf9a90c | 238 | |
17ba0788 | 239 | \rare{--parse-error-msg}{Show parsing errors in the C file.} |
faf9a90c | 240 | |
17ba0788 | 241 | \rare{--verbose-parsing}{Show parsing errors in the C file, as well as |
ae4735db | 242 | information about attempts to accomodate such errors. This implicitly |
17ba0788 | 243 | sets --parse-error-msg.} |
ae4735db | 244 | |
17ba0788 | 245 | \rare{--type-error-msg}{Show information about where the C type checker |
faf9a90c C |
246 | was not able to determine the type of an expression.} |
247 | ||
17ba0788 | 248 | \rare{--int-bits $\langle$n$\rangle$, --long-bits |
708f4980 C |
249 | $\langle$n$\rangle$}{Provide integer size information. n is the number of |
250 | bits in an unsigned integer or unsigned long, respectively. If only the | |
17ba0788 | 251 | option {\bf --int-bits} is used, unsigned longs will be assumed to have |
708f4980 | 252 | twice as many bits as unsigned integers. If only the option {\bf |
17ba0788 | 253 | -long-bits} is used, unsigned ints will be assumed to have half as many |
708f4980 C |
254 | bits as unsigned integers. This information is only used in determining |
255 | the types of integer constants, according to the ANSI C standard (C89). If | |
256 | neither is provided, the type of an integer constant is determined by the | |
257 | sequence of ``u'' and ``l'' annotations following the constant. If there | |
258 | is none, the constant is assumed to be a signed integer. If there is only | |
259 | ``u'', the constant is assumed to be an unsigned integer, etc.} | |
260 | ||
17ba0788 | 261 | \rare{--no-loops}{Drop back edges for loops. This may make a semantic |
002099fc C |
262 | patch/match run faster, at the cost of not finding matches that wrap |
263 | around loops.} | |
264 | ||
17ba0788 | 265 | \developer{--use-cache}{Use preparsed versions of the C files that are |
5427db06 C |
266 | stored in a cache.} |
267 | ||
17ba0788 C |
268 | \developer{--cache-prefix}{Specify the directory in which to store |
269 | preparsed versions of the C files. This sets {--use-cache}} | |
faf9a90c | 270 | |
17ba0788 | 271 | \developer{--cache-limit}{Specify the maximum number of |
f3c4ece6 | 272 | preparsed C files to store. The cache is cleared of all files with names |
17ba0788 C |
273 | ending in .ast-raw and .depend-raw on reaching this limit. Only |
274 | effective if --cache-prefix is used as well. This is most useful when | |
f3c4ece6 C |
275 | iteration is used to process a file multiple times within a single run of |
276 | Coccinelle.} | |
277 | ||
17ba0788 C |
278 | \developer{--debug-cpp, --debug-lexer, --debug-etdt, |
279 | --debug-typedef}{Various options for debugging the C parser.} | |
faf9a90c | 280 | |
17ba0788 C |
281 | \developer{--filter-msg, --filter-define-error, |
282 | --filter-passed-level}{Various options for debugging the C parser.} | |
faf9a90c | 283 | |
17ba0788 | 284 | \developer{--only-return-is-error-exit}{In matching ``{\tt{\ldots}}'' in |
faf9a90c C |
285 | a semantic patch or when forall is specified, a rule must match all |
286 | control-flow paths starting from a node matching the beginning of the | |
287 | rule. This is relaxed, however, for error handling code. Normally, error | |
288 | handling code is considered to be a conditional with only a then branch | |
289 | that ends in goto, break, continue, or return. If this option is set, | |
290 | then only a then branch ending in a return is considered to be error | |
291 | handling code. Usually a better strategy is to use {\tt when strict} in | |
292 | the semantic patch, and then match explicitly the case where there is a | |
293 | conditional whose then branch ends in a return.} | |
294 | ||
295 | \subsubsection*{Macros and other preprocessor code} | |
296 | ||
17ba0788 | 297 | \normal{--macro-file $\langle$file$\rangle$}{ |
faf9a90c | 298 | Extra macro definitions to be taken into account when parsing the C |
18b1275a C |
299 | files. This uses the provided macro definitions in addition to those in |
300 | the default macro file.} | |
faf9a90c | 301 | |
17ba0788 | 302 | \normal{--macro-file-builtins $\langle$file$\rangle$}{ |
708f4980 | 303 | Builtin macro definitions to be taken into account when parsing the C |
18b1275a C |
304 | files. This causes the macro definitions provided in the default macro |
305 | file to be ignored and the ones in the specified file to be used instead.} | |
708f4980 | 306 | |
17ba0788 C |
307 | \rare{--ifdef-to-if,-no-ifdef-to-if}{ |
308 | The option {\bf --ifdef-to-if} | |
708f4980 C |
309 | represents an {\tt \#ifdef} in the source code as a conditional in the |
310 | control-flow graph when doing so represents valid code. {\bf | |
17ba0788 | 311 | -no-ifdef-to-if} disables this feature. {\bf --ifdef-to-if} is the |
708f4980 C |
312 | default. |
313 | } | |
faf9a90c | 314 | |
17ba0788 | 315 | \rare{--use-if0-code}{ Normally code under \#if 0 is ignored. If this |
faf9a90c C |
316 | option is set then the code is considered, just like the code under any |
317 | other \#ifdef.} | |
318 | ||
17ba0788 | 319 | \developer{--noadd-typedef-root}{This seems to reduce the scope of a |
faf9a90c C |
320 | typedef declaration found in the C code.} |
321 | ||
322 | \subsubsection*{Include files} | |
323 | ||
17ba0788 C |
324 | \normal{--recursive-includes, --all-includes, --local-includes, |
325 | --no-includes}{ These options control which include files mentioned in a | |
326 | C file are taken into account. {\bf --recursive-includes} indicates | |
1eddfd50 | 327 | that all included files mentioned in the .c file(s) or any included files |
17ba0788 | 328 | will be processed. {\bf --all-includes} indicates that all included |
1eddfd50 | 329 | files mentioned in the .c file(s) will be processed. {\bf |
17ba0788 C |
330 | --local-includes} indicates that only included files in the current |
331 | directory will be processed. {\bf --no-includes} indicates that no | |
1eddfd50 C |
332 | included files will be processed. If the semantic patch contains type |
333 | specifications on expression metavariables, then the default is {\bf | |
17ba0788 | 334 | --local-includes}. Otherwise the default is {\bf --no-includes}. At |
1eddfd50 | 335 | most one of these options can be specified.} |
faf9a90c | 336 | |
5636bb2c C |
337 | \normal{-I $\langle$path$\rangle$}{ This option specifies a directory |
338 | in which to find non-local include files. This option can be used | |
339 | several times.} | |
faf9a90c | 340 | |
17ba0788 | 341 | \rare{--relax-include-path}{This option when combined with --all-includes |
7f004419 | 342 | causes the search for local |
aba5c457 C |
343 | include files to consider the current directory, even if the include |
344 | patch specifies a subdirectory. This is really only useful for testing, | |
17ba0788 | 345 | eg with the option {\bf --testall}} |
faf9a90c | 346 | |
17ba0788 | 347 | \rare{--c++}{Make an extremely minimal effort to parse C++ code. Currently, |
3a314143 C |
348 | this is limited to allowing identifiers to contain ``::'', tilde, and |
349 | template invocations. Consider testing your code first with spatch | |
17ba0788 | 350 | --type-c to see if there are any type annotations in the code you are |
3a314143 C |
351 | interested in processing. If not, then it was probably not parsed.} |
352 | ||
faf9a90c C |
353 | \section{Application of the semantic patch to the C code} |
354 | ||
355 | \subsection{Feedback at the rule level during the application of the | |
356 | semantic patch} | |
357 | ||
17ba0788 | 358 | \normal{--show-bindings}{ |
faf9a90c C |
359 | Show the environments with respect to which each rule is applied and the |
360 | bindings that result from each such application.} | |
361 | ||
17ba0788 C |
362 | \normal{--show-dependencies}{ Show the status (matched or unmatched) of the |
363 | rules on which a given rule depends. {\bf --show-dependencies} implicitly | |
364 | sets {\bf --show-bindings}, as the values of the dependencies are | |
faf9a90c C |
365 | environment-specific.} |
366 | ||
17ba0788 | 367 | \normal{--show-trying}{ |
faf9a90c C |
368 | Show the name of each program element to which each rule is applied.} |
369 | ||
17ba0788 | 370 | \normal{--show-transinfo}{ |
faf9a90c C |
371 | Show information about each transformation that is performed. |
372 | The node numbers that are referenced are the number of the nodes in the | |
17ba0788 C |
373 | control-flow graph, which can be seen using the option {\bf --control-flow} |
374 | (the initial control-flow graph only) or the option {\bf --show-flow} (the | |
faf9a90c C |
375 | control-flow graph before and after each rule application).} |
376 | ||
17ba0788 | 377 | \normal{--show-misc}{Show some miscellaneous information.} |
faf9a90c | 378 | |
17ba0788 | 379 | \rare{--show-flow $\langle$file$\rangle$, --show-flow |
faf9a90c C |
380 | $\langle$file$\rangle$:$\langle$function$\rangle$} Show the control-flow |
381 | graph before and after the application of each rule. | |
382 | ||
17ba0788 C |
383 | \developer{--show-before-fixed-flow}{This is similar to {\bf |
384 | --show-flow}, but shows a preliminary version of the control-flow graph.} | |
faf9a90c C |
385 | |
386 | \subsection{Feedback at the CTL level during the application of the | |
387 | semantic patch} | |
388 | ||
17ba0788 | 389 | \normal{--verbose-engine}{Show a trace of the matching of atomic terms to C |
faf9a90c C |
390 | code.} |
391 | ||
17ba0788 | 392 | \rare{--verbose-ctl-engine}{Show a trace of the CTL matching process. |
faf9a90c C |
393 | This is unfortunately rather voluminous and not so helpful for someone |
394 | who is not familiar with CTL in general and the translation of SmPL into | |
395 | CTL specifically. This option implicitly sets the option {\bf | |
17ba0788 | 396 | --show-ctl-text}.} |
faf9a90c | 397 | |
17ba0788 | 398 | \rare{--graphical-trace}{Create a pdf file containing the control flow |
faf9a90c C |
399 | graph annotated with the various nodes matched during the CTL matching |
400 | process. Unfortunately, except for the most simple examples, the output | |
401 | is voluminous, and so the option is not really practical for most | |
402 | examples. This requires {\tt dot} (http://www.graphviz.org/) and {\tt | |
403 | pdftk}.} | |
404 | ||
17ba0788 | 405 | \rare{--gt-without-label}{The same as {\bf --graphical-trace}, but the PDF |
faf9a90c C |
406 | file does not contain the CTL code.} |
407 | ||
17ba0788 | 408 | \rare{--partial-match}{ |
faf9a90c C |
409 | Report partial matches of the semantic patch on the C file. This can |
410 | be substantially slower than normal matching.} | |
411 | ||
17ba0788 | 412 | \rare{--verbose-match}{ |
faf9a90c C |
413 | Report on when CTL matching is not applied to a function or other program |
414 | unit because it does not contain some required atomic pattern. | |
415 | This can be viewed as a simpler, more efficient, but less informative | |
17ba0788 | 416 | version of {\bf --partial-match}.} |
faf9a90c C |
417 | |
418 | \subsection{Actions during the application of the semantic patch} | |
419 | ||
ae4735db C |
420 | \normal{-D rulename}{Run the patch considering that the virtual rule |
421 | ``rulename'' is satisfied. Virtual rules should be declared at the | |
422 | beginning of the semantic patch in a comma separated list following the | |
423 | keyword virtual. Other rules can depend on the satisfaction or non | |
424 | satifaction of these rules using the keyword {\tt depends on} in the | |
425 | usual way.} | |
426 | ||
427 | \normal{-D variable=value}{Run the patch considering that the virtual | |
428 | identifier metavariable ``variable'' is bound to ``value''. Any | |
429 | identifier metavariable can be designated as being virtual by giving it | |
430 | the rule name {\tt virtual}. An example is in demos/vm.coci} | |
431 | ||
17ba0788 | 432 | \rare{--allow-inconsistent-paths}{Normally, a term that is transformed |
faf9a90c C |
433 | should only be accessible from other terms that are matched by the |
434 | semantic patch. This option removes this constraint. Doing so, is | |
435 | unsafe, however, because the properties that hold along the matched path | |
436 | might not hold at all along the unmatched path.} | |
437 | ||
17ba0788 | 438 | \rare{--disallow-nested-exps}{In an expression that contains repeated |
faf9a90c C |
439 | nested subterms, {\em e.g.} of the form {\tt f(f(x))}, a pattern can |
440 | match a single expression in multiple ways, some nested inside others. | |
441 | This option causes the matching process to stop immediately at the | |
442 | outermost match. Thus, in the example {\tt f(f(x))}, the possibility | |
443 | that the pattern {\tt f(E)}, with metavariable {\tt E}, matches with {\tt | |
444 | E} as {\tt x} will not be considered.} | |
445 | ||
17ba0788 | 446 | \rare{--no-safe-expressions}{normally, we check that an expression does |
978fd7e5 C |
447 | not match something earlier in the disjunction. But for large |
448 | disjunctions, this can result in a very big CTL formula. So this | |
449 | option give the user the option to say he doesn't want this feature, | |
450 | if that is the case.} | |
451 | ||
17ba0788 | 452 | \rare{--pyoutput coccilib.output.Gtk, --pyoutput coccilib.output.Console}{ |
faf9a90c | 453 | This controls whether Python output is sent to Gtk or to the console. {\bf |
17ba0788 | 454 | --pyoutput coccilib.output.Console} is the default. The Gtk option is |
faf9a90c C |
455 | currently not well supported.} |
456 | ||
17ba0788 | 457 | \developer{--loop}{When there is ``{\tt{\ldots}}'' in the semantic patch, |
faf9a90c C |
458 | the CTL operator {\sf AU} is used if the current function does not |
459 | contain a loop, and {\sf AW} may be used if it does. This option causes | |
460 | {\sf AW} always to be used.} | |
461 | ||
17ba0788 | 462 | \rare{--ocaml-regexps}{Use the regular expressions provided by the OCaml |
993936c0 C |
463 | \texttt{Str} library. This is the default if the PCRE library is not |
464 | available. Otherwise PCRE regular expressions are used by default.} | |
465 | ||
17ba0788 | 466 | \developer{--steps $\langle$int$\rangle$}{ |
faf9a90c C |
467 | This limits the number of steps performed by the CTL engine to the |
468 | specified number. This option is unsafe as it might cause a rule to fail | |
469 | due to running out of steps rather than due to not matching.} | |
470 | ||
17ba0788 | 471 | \developer{--bench $\langle$int$\rangle$}{This collects various information |
faf9a90c C |
472 | about the operations performed during the CTL matching process.} |
473 | ||
17ba0788 C |
474 | % \developer{--popl, --popl-mark-all, --popl-keep-all-wits}{ |
475 | % These options use a simplified version of the SmPL language. {\bf | |
476 | % --popl-mark-all} and {\bf --popl-keep-all-wits} implicitly set {\bf | |
477 | % --popl}.} | |
faf9a90c C |
478 | |
479 | \section{Generation of the result} | |
480 | ||
6756e19d C |
481 | Normally, the only output is a diff printed to standard output, containing |
482 | the differences between the original code and the transformed code. If | |
483 | stars are used in column 0 rather than {\tt -} and {\tt +}, then the {\tt | |
484 | -} lines in the diff are the lines that matched the stars. | |
faf9a90c | 485 | |
17ba0788 | 486 | \normal{--keep-comments}{Don't remove comments adjacent to removed code.} |
7f004419 | 487 | |
17ba0788 C |
488 | \normal{--linux-spacing, --smpl-spacing}{Control the spacing within the code |
489 | added by the semantic patch. The option {\bf --linux-spacing} causes | |
708f4980 C |
490 | spatch to follow the conventions of Linux, regardless of the spacing in |
491 | the semantic patch. This is the default. The option {\bf | |
17ba0788 | 492 | --smpl-spacing} causes spatch to follow the spacing given in the semantic |
708f4980 C |
493 | patch, within individual lines.} |
494 | ||
6756e19d C |
495 | \rare{-o $\langle$file$\rangle$}{ This causes the transformed code to be |
496 | placed in the file {\tt file}. A diff is still printed to the standard | |
497 | output. This option only makes sense when {\tt -} and {\tt +} are used.} | |
faf9a90c | 498 | |
17ba0788 | 499 | \rare{--in-place}{ Modify the input file to contain the transformed code. |
6756e19d C |
500 | A diff is still printed to the standard output. By default, the input |
501 | file is overwritten when using this option, with no backup. This option | |
502 | only makes sense when {\tt -} and {\tt +} are used.} | |
faf9a90c | 503 | |
17ba0788 | 504 | \rare{--backup-suffix}{The suffix of the file to use in making a backup of |
5636bb2c C |
505 | the original file(s). This suffix should include the leading ``.'', if |
506 | one is desired. This option only has an effect when the option | |
17ba0788 | 507 | {\tt --in-place} is also used.} |
5636bb2c | 508 | |
17ba0788 | 509 | \rare{--out-place}{ Store the result of modifying the code in a .cocci-res |
6756e19d C |
510 | file. A diff is still printed to the standard output. This option only |
511 | makes sense when {\tt -} and {\tt +} are used.} | |
faf9a90c | 512 | |
17ba0788 | 513 | \rare{--no-show-diff}{ Normally, a diff between the original and transformed |
faf9a90c C |
514 | code is printed on the standard output. This option causes this not to be |
515 | done.} | |
516 | ||
517 | \rare{-U}{ Set number of diff context lines.} | |
518 | ||
17ba0788 | 519 | \rare{--patch $\langle$path$\rangle$}{The prefix of the pathname of the |
c3e37e97 C |
520 | directory or file name that should dropped from the diff line in the |
521 | generated patch. This is useful if you want to apply a patch only to a | |
522 | subdirectory of a source code tree but want to create a patch that can be | |
523 | applied at the root of the source code tree. An example could be {\tt | |
17ba0788 | 524 | spatch --sp-file foo.cocci --dir /var/linuxes/linux-next/drivers --patch |
c3e37e97 C |
525 | /var/linuxes/linux-next}. A trailing {\tt /} is permitted on the |
526 | directory name and has no impact on the result.} | |
527 | ||
17ba0788 | 528 | \rare{--save-tmp-files}{Coccinelle creates some temporary |
faf9a90c C |
529 | files in {\tt /tmp} that it deletes after use. This option causes these |
530 | files to be saved.} | |
531 | ||
17ba0788 | 532 | \developer{--debug-unparsing}{Show some debugging information about the |
faf9a90c C |
533 | generation of the transformed code. This has the side-effect of |
534 | deleting the transformed code.} | |
535 | ||
faf9a90c C |
536 | |
537 | \section{Other options} | |
538 | ||
539 | \subsection{Version information} | |
540 | ||
17ba0788 | 541 | \normal{--version}{ The version of Coccinelle. No other options are |
faf9a90c C |
542 | allowed.} |
543 | ||
17ba0788 | 544 | \normal{--date}{ The date of the current version of Coccinelle. No other |
faf9a90c C |
545 | options are allowed.} |
546 | ||
547 | \subsection{Help} | |
548 | ||
17ba0788 | 549 | \minimum{--h, --shorthelp}{ The most useful commands.} |
faf9a90c | 550 | |
17ba0788 | 551 | \minimum{--help, --help, --longhelp}{ A complete listing of the available |
faf9a90c C |
552 | commands.} |
553 | ||
554 | \subsection{Controlling the execution of Coccinelle} | |
555 | ||
17ba0788 | 556 | \normal{--timeout $\langle$int$\rangle$}{ The maximum time in seconds for |
faf9a90c C |
557 | processing a single file.} |
558 | ||
17ba0788 | 559 | \rare{--max $\langle$int$\rangle$}{This option informs Coccinelle of the |
faf9a90c | 560 | number of instances of Coccinelle that will be run concurrently. This |
17ba0788 | 561 | option requires {\bf --index}. It is usually used with {\bf --dir}.} |
faf9a90c | 562 | |
17ba0788 | 563 | \rare{--index $\langle$int$\rangle$}{This option informs Coccinelle of |
faf9a90c | 564 | which of the concurrent instances is the current one. This option |
17ba0788 | 565 | requires {\bf --max}.} |
faf9a90c | 566 | |
17ba0788 | 567 | \rare{--mod-distrib}{When multiple instances of Coccinelle are run in |
faf9a90c C |
568 | parallel, normally the first instance processes the first $n$ files, the |
569 | second instance the second $n$ files, etc. With this option, the files | |
570 | are distributed among the instances in a round-robin fashion.} | |
571 | ||
17ba0788 | 572 | \developer{--debugger}{Option for running Coccinelle from within the OCaml |
faf9a90c C |
573 | debugger.} |
574 | ||
17ba0788 | 575 | \developer{--profile}{ Gather timing information about the main Coccinelle |
faf9a90c C |
576 | functions.} |
577 | ||
17ba0788 | 578 | \developer{--disable-once}{Print various warning messages every time some |
faf9a90c C |
579 | condition occurs, rather than only once.} |
580 | ||
581 | \subsection{Miscellaneous} | |
582 | ||
17ba0788 | 583 | \rare{--quiet}{Suppress most output. This is the default.} |
faf9a90c | 584 | |
17ba0788 C |
585 | %\developer{--pad, -hrule $\langle$dir$\rangle$, -xxx, -l1}{} |
586 | \developer{--pad, --xxx, --l1}{} | |
faf9a90c | 587 | |
5636bb2c C |
588 | |
589 | %%% Local Variables: | |
590 | %%% mode: LaTeX | |
591 | %%% TeX-master: "main_options" | |
592 | %%% coding: utf-8 | |
593 | %%% TeX-PDF-mode: t | |
594 | %%% ispell-local-dictionary: "american" | |
595 | %%% End: |