3 This
document describes the options provided by Coccinelle. The options
4 have an impact on various phases of the semantic patch application
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.
12 \item Generation of the result.
16 One can either initiate the complete process from step
1, or
17 to perform step
1 or step
2 individually.
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
}:
24 \item {\tt spatch -parse
\_cocci foo.cocci
}: Check that the semantic patch
25 is syntactically correct.
26 \item {\tt spatch -parse
\_c foo.c
}: Check that the C file
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
32 \item {\tt spatch -sp
\_file foo.cocci foo.c
}: Apply the semantic patch
{\tt
33 foo.cocci
} to the file
{\tt foo.c
} and print out any transformations as a
35 \item {\tt spatch -sp
\_file foo.cocci foo.c -debug
}: The same as the
36 previous case, but print out some information about the matching process.
37 \item {\tt spatch -sp
\_file foo.cocci -dir foodir
}: Apply the semantic
38 patch
{\tt foo.cocci
} to all of the C files in the directory
{\tt foodir
}.
39 \item {\tt spatch -sp
\_file foo.cocci -dir foodir -include
\_headers}: Apply
40 the semantic patch
{\tt foo.cocci
} to all of the C files and header files
41 in the directory
{\tt foodir
}.
44 In the rest of this
document, the options are annotated as follows:
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
56 \section{Selecting and parsing the semantic patch
}
58 \subsection{Standalone options
}
60 \normal{-parse
\_cocci $
\langle$file$
\rangle$
}{ Parse a semantic
61 patch file and print out some information about it.
}
63 \subsection{The semantic patch
}
65 \minimum{-sp
\_file $
\langle$file$
\rangle$, -c $
\langle$file$
\rangle$,
66 -cocci
\_file $
\langle$file$
\rangle$
}{ Specify the name of the file
67 containing the semantic patch. The file name should end in
{\tt .cocci
}.
68 All three options do the same thing; the last two are deprecated.
}
70 \subsection{Isomorphisms
}
72 \rare{-iso, -iso
\_file}{ Specify a file containing isomorphisms to be used in
73 place of the standard one. Normally one should use the
{\tt using
}
74 construct within a semantic patch to specify isomorphisms to be used
{\em
75 in addition to
} the standard ones.
}
77 \rare{-iso
\_limit $
\langle$int$
\rangle$
} Limit the depth of application of
78 isomorphisms to the specified integer.
80 \rare{-no
\_iso\_limit} Put no limit on the number of times that
81 isomorphisms can be applied. This is the default.
83 \developer{-track
\_iso}{ Gather information about isomorphism usage.
}
85 \developer{-profile
\_iso}{ Gather information about the time required for
86 isomorphism expansion.
}
88 \subsection{Display options
}
90 \rare{-show
\_cocci}{Show the semantic patch that is being processed before
91 expanding isomorphisms.
}
93 \rare{-show
\_SP}{Show the semantic patch that is being processed after
94 expanding isomorphisms.
}
96 \rare{-show
\_ctl\_text}{ Show the representation
97 of the semantic patch in CTL.
}
99 \rare{-ctl
\_inline\_let}{ Sometimes
{\tt let
} is used to name
100 intermediate terms CTL representation. This option causes the let-bound
101 terms to be inlined at the point of their reference.
102 This option implicitly sets
{\bf -show
\_ctl\_text}.
}
104 \rare{-ctl
\_show\_mcodekind}{ Show
105 transformation information within the CTL representation
106 of the semantic patch. This option implicitly sets
{\bf -show
\_ctl\_text}.
}
108 \rare{-show
\_ctl\_tex}{ Create a LaTeX files showing the representation
109 of the semantic patch in CTL.
}
111 \section{Selecting and parsing the C files
}
113 \subsection{Standalone options
}
115 \normal{-parse
\_c $
\langle$file/dir$
\rangle$
}{ Parse a
{\tt .c
} file or all
116 of the
{\tt .c
} files in a directory. This generates information about
117 any parse errors encountered.
}
119 \normal{-parse
\_h $
\langle$file/dir$
\rangle$
}{ Parse a
{\tt .h
} file or all
120 of the
{\tt .h
} files in a directory. This generates information about
121 any parse errors encountered.
}
123 \normal{-parse
\_ch $
\langle$file/dir$
\rangle$
}{ Parse a
{\tt .c
} or
{\tt
124 .h
} file or all of the
{\tt .c
} or
{\tt .h
} files in a directory. This
125 generates information about any parse errors encountered.
}
127 \normal{-control
\_flow $
\langle$file$
\rangle$, -control
\_flow
128 $
\langle$file$
\rangle$:$
\langle$function$
\rangle$
}{ Print a control-flow
129 graph for all of the functions in a file or for a specific function in a
130 file. This requires
{\tt dot
} (http://www.graphviz.org/) and
{\tt gv
}.
}
132 \rare{-type
\_c $
\langle$file$
\rangle$
}{ Parse a C file and pretty-print a
133 version including type information.
}
135 \developer{-tokens
\_c $
\langle$file$
\rangle$
}{Prints the tokens in a C
138 \developer{-parse
\_unparse $
\langle$file$
\rangle$
}{Parse and then reconstruct
141 \developer{-compare
\_c $
\langle$file$
\rangle$ $
\langle$file$
\rangle$,
142 -compare
\_c\_hardcoded}{Compares one C file to another, or compare the
143 file tests/compare1.c to the file tests/compare2.c.
}
145 \developer{-test
\_cfg\_ifdef $
\langle$file$
\rangle$
}{Do some special
146 processing of \#ifdef and display the resulting control-flow graph. This
147 requires
{\tt dot
} and
{\tt gv
}.
}
149 \developer{-test
\_attributes $
\langle$file$
\rangle$,
150 -test
\_cpp $
\langle$file$
\rangle$
}{
151 Test the parsing of cpp code and attributes, respectively.
}
153 \subsection{Selecting C files
}
155 An argument that ends in
{\tt .c
} is assumed to be a C file to process.
156 Normally, only one C file or one directory is specified. If multiple C
157 files are specified, they are treated in parallel,
{\em i.e.
}, the first
158 semantic patch rule is applied to all functions in all files, then the
159 second semantic patch rule is applied to all functions in all files, etc.
160 If a directory is specified then no files may be specified and only the
161 rightmost directory specified is used.
163 \normal{-include
\_headers}{ This option causes header files to be processed
164 independently. This option only makes sense if a directory is specified
167 \normal{-use
\_glimpse}{ Use a glimpse index to select the files to which
168 a semantic patch may be relevant. This option requires that a directory is
169 specified. The index may be created using the script
{\tt
170 coccinelle/scripts/ glimpseindex
\_cocci.sh
}. Glimpse is available at
171 http://webglimpse.net/. In conjunction with the option
{\bf -patch
\_cocci}
172 this option prints the regular expression that will be passed to glimpse.
}
174 \rare{-dir
}{ Specify a directory containing C files to process. By
175 default, the include path will be set to the ``include'' subdirectory of
176 this directory. A different include path can be specified using the
177 option
{\bf -I
}.
{\bf -dir
} only considers the rightmost directory in
178 the argument list. This behavior is convenient for creating a script
179 that always works on a single directory, but allows the user of the
180 script to override the provided directory with another one. Spatch
181 collects the files in the directory using
{\tt find
} and does not follow
184 \developer{-kbuild
\_info $
\langle$file$
\rangle$
}{ The specified file
185 contains information about which sets of files should be considered in
188 \developer{-disable
\_worth\_trying\_opt}{Normally, a C file is only
189 processed if it contains some keywords that have been determined to be
190 essential for the semantic patch to match somewhere in the file. This
191 option disables this optimization and tries the semantic patch on all files.
}
193 \developer{-test $
\langle$file$
\rangle$
}{ A shortcut for running Coccinelle
194 on the semantic patch ``file
{\tt{.cocci
}}'' and the C file ``file
{\tt{.c
}}''.
}
196 \developer{-testall
}{A shortcut for running Coccinelle on all files in a
197 subdirectory
{\tt tests
} such that there are all of a
{\tt .cocci
} file, a
{\tt
198 .c
} file, and a
{\tt .res
} file, where the
{\tt .res
} contains the
201 \developer{-test
\_okfailed, -test
\_regression\_okfailed} Other options for
202 keeping track of tests that have succeeded and failed.
204 \developer{-compare
\_with\_expected}{Compare the result of applying
205 Coccinelle to file
{\tt{.c
}} to the file file
{\tt{.res
}} representing the
208 \developer{-expected
\_score\_file $
\langle$file$
\rangle$
}{
209 which score file to compare with in the testall run
}
211 \subsection{Parsing C files
}
213 \rare{-show
\_c}{Show the C code that is being processed.
}
215 \rare{-parse
\_error\_msg}{Show parsing errors in the C file.
}
217 \rare{-type
\_error\_msg}{Show information about where the C type checker
218 was not able to determine the type of an expression.
}
220 \rare{-int
\_bits $
\langle$n$
\rangle$, -long
\_bits
221 $
\langle$n$
\rangle$
}{Provide integer size information. n is the number of
222 bits in an unsigned integer or unsigned long, respectively. If only the
223 option
{\bf -int
\_bits} is used, unsigned longs will be assumed to have
224 twice as many bits as unsigned integers. If only the option
{\bf
225 -long
\_bits} is used, unsigned ints will be assumed to have half as many
226 bits as unsigned integers. This information is only used in determining
227 the types of integer constants, according to the ANSI C standard (C89). If
228 neither is provided, the type of an integer constant is determined by the
229 sequence of ``u'' and ``l'' annotations following the constant. If there
230 is none, the constant is assumed to be a signed integer. If there is only
231 ``u'', the constant is assumed to be an unsigned integer, etc.
}
233 \developer{-use
\_cache} Use preparsed versions of the C files that are
236 \developer{-debug
\_cpp, -debug
\_lexer, -debug
\_etdt,
237 -debug
\_typedef}{Various options for debugging the C parser.
}
239 \developer{-filter
\_msg, -filter
\_define\_error,
240 -filter
\_passed\_level}{Various options for debugging the C parser.
}
242 \developer{-only
\_return\_is\_error\_exit}{In matching ``
{\tt{\ldots}}'' in
243 a semantic patch or when forall is specified, a rule must match all
244 control-flow paths starting from a node matching the beginning of the
245 rule. This is relaxed, however, for error handling code. Normally, error
246 handling code is considered to be a conditional with only a then branch
247 that ends in goto, break, continue, or return. If this option is set,
248 then only a then branch ending in a return is considered to be error
249 handling code. Usually a better strategy is to use
{\tt when strict
} in
250 the semantic patch, and then match explicitly the case where there is a
251 conditional whose then branch ends in a return.
}
253 \subsubsection*
{Macros and other preprocessor code
}
255 \normal{-macro
\_file $
\langle$file$
\rangle$
}{
256 Extra macro definitions to be taken into account when parsing the C
259 \normal{-macro
\_file\_builtins $
\langle$file$
\rangle$
}{
260 Builtin macro definitions to be taken into account when parsing the C
263 \rare{-ifdef
\_to\_if,-no
\_ifdef\_to\_if}{
264 The option
{\bf -ifdef
\_to\_if}
265 represents an
{\tt \#ifdef
} in the source code as a conditional in the
266 control-flow graph when doing so represents valid code.
{\bf
267 -no
\_ifdef\_to\_if} disables this feature.
{\bf -ifdef
\_to\_if} is the
271 \rare{-use
\_if0\_code}{ Normally code under \#if
0 is ignored. If this
272 option is set then the code is considered, just like the code under any
275 \developer{-noadd
\_typedef\_root}{This seems to reduce the scope of a
276 typedef declaration found in the C code.
}
278 \subsubsection*
{Include files
}
280 \normal{-all
\_includes, -local
\_includes, -no
\_includes}{
281 These options control which include files mentioned in a C file are taken into
282 account.
{\bf -all
\_includes} indicates that all included files will be
283 processed.
{\bf -local
\_includes} indicates that only included files in
284 the current directory will be processed.
{\bf -no
\_includes} indicates
285 that no included files will be processed. If the semantic patch contains
286 type specifications on expression metavariables, then the default is
{\bf
287 -local
\_includes}. Otherwise the default is
{\bf -no
\_includes}. At most
288 one of these options can be specified.
}
290 \normal{-I $
\langle$path$
\rangle$
}{ This option specifies the directory in
291 which to find non-local include files. This option should be used only
292 once, as each use will overwrite the preceding one.
}
294 \rare{-relax
\_include\_path}{This option causes the search for local
295 include files to consider the directory specified using
{\bf -I
} if the
296 included file is not found in the current directory.
}
298 \section{Application of the semantic patch to the C code
}
300 \subsection{Feedback at the rule level during the application of the
303 \normal{-show
\_bindings}{
304 Show the environments with respect to which each rule is applied and the
305 bindings that result from each such application.
}
307 \normal{-show
\_dependencies}{ Show the status (matched or unmatched) of the
308 rules on which a given rule depends.
{\bf -show
\_dependencies} implicitly
309 sets
{\bf -show
\_bindings}, as the values of the dependencies are
310 environment-specific.
}
312 \normal{-show
\_trying}{
313 Show the name of each program element to which each rule is applied.
}
315 \normal{-show
\_transinfo}{
316 Show information about each transformation that is performed.
317 The node numbers that are referenced are the number of the nodes in the
318 control-flow graph, which can be seen using the option
{\bf -control
\_flow}
319 (the initial control-flow graph only) or the option
{\bf -show
\_flow} (the
320 control-flow graph before and after each rule application).
}
322 \normal{-show
\_misc}{Show some miscellaneous information.
}
324 \rare{-show
\_flow $
\langle$file$
\rangle$, -show
\_flow
325 $
\langle$file$
\rangle$:$
\langle$function$
\rangle$
} Show the control-flow
326 graph before and after the application of each rule.
328 \developer{-show
\_before\_fixed\_flow}{This is similar to
{\bf
329 -show
\_flow}, but shows a preliminary version of the control-flow graph.
}
331 \subsection{Feedback at the CTL level during the application of the
334 \normal{-verbose
\_engine}{Show a trace of the matching of atomic terms to C
337 \rare{-verbose
\_ctl\_engine}{Show a trace of the CTL matching process.
338 This is unfortunately rather voluminous and not so helpful for someone
339 who is not familiar with CTL in general and the translation of SmPL into
340 CTL specifically. This option implicitly sets the option
{\bf
343 \rare{-graphical
\_trace}{Create a pdf file containing the control flow
344 graph annotated with the various nodes matched during the CTL matching
345 process. Unfortunately, except for the most simple examples, the output
346 is voluminous, and so the option is not really practical for most
347 examples. This requires
{\tt dot
} (http://www.graphviz.org/) and
{\tt
350 \rare{-gt
\_without\_label}{The same as
{\bf -graphical
\_trace}, but the PDF
351 file does not contain the CTL code.
}
353 \rare{-partial
\_match}{
354 Report partial matches of the semantic patch on the C file. This can
355 be substantially slower than normal matching.
}
357 \rare{-verbose
\_match}{
358 Report on when CTL matching is not applied to a function or other program
359 unit because it does not contain some required atomic pattern.
360 This can be viewed as a simpler, more efficient, but less informative
361 version of
{\bf -partial
\_match}.
}
363 \subsection{Actions during the application of the semantic patch
}
365 \rare{-allow
\_inconsistent\_paths}{Normally, a term that is transformed
366 should only be accessible from other terms that are matched by the
367 semantic patch. This option removes this constraint. Doing so, is
368 unsafe, however, because the properties that hold along the matched path
369 might not hold at all along the unmatched path.
}
371 \rare{-disallow
\_nested\_exps}{In an expression that contains repeated
372 nested subterms,
{\em e.g.
} of the form
{\tt f(f(x))
}, a pattern can
373 match a single expression in multiple ways, some nested inside others.
374 This option causes the matching process to stop immediately at the
375 outermost match. Thus, in the example
{\tt f(f(x))
}, the possibility
376 that the pattern
{\tt f(E)
}, with metavariable
{\tt E
}, matches with
{\tt
377 E
} as
{\tt x
} will not be considered.
}
379 \rare{-pyoutput coccilib.output.Gtk, -pyoutput coccilib.output.Console
}{
380 This controls whether Python output is sent to Gtk or to the console.
{\bf
381 -pyoutput coccilib.output.Console
} is the default. The Gtk option is
382 currently not well supported.
}
384 \developer{-loop
}{When there is ``
{\tt{\ldots}}'' in the semantic patch,
385 the CTL operator
{\sf AU
} is used if the current function does not
386 contain a loop, and
{\sf AW
} may be used if it does. This option causes
387 {\sf AW
} always to be used.
}
389 \developer{-steps $
\langle$int$
\rangle$
}{
390 This limits the number of steps performed by the CTL engine to the
391 specified number. This option is unsafe as it might cause a rule to fail
392 due to running out of steps rather than due to not matching.
}
394 \developer{-bench $
\langle$int$
\rangle$
}{This collects various information
395 about the operations performed during the CTL matching process.
}
397 \developer{-popl, -popl
\_mark\_all, -popl
\_keep\_all\_wits}{
398 These options use a simplified version of the SmPL language.
{\bf
399 -popl
\_mark\_all} and
{\bf -popl
\_keep\_all\_wits} implicitly set
{\bf
402 \section{Generation of the result
}
404 Normally, the only output is a diff printed to standard output.
406 \normal{-linux
\_spacing, -smpl
\_spacing}{Control the spacing within the code
407 added by the semantic patch. The option
{\bf -linux
\_spacing} causes
408 spatch to follow the conventions of Linux, regardless of the spacing in
409 the semantic patch. This is the default. The option
{\bf
410 -smpl
\_spacing} causes spatch to follow the spacing given in the semantic
411 patch, within individual lines.
}
413 \rare{-o $
\langle$file$
\rangle$
}{ The output file.
}
415 \rare{-inplace
}{ Modify the input file.
}
417 \rare{-outplace
}{ Store modifications in a .cocci
\_res file.
}
419 \rare{-no
\_show\_diff}{ Normally, a diff between the original and transformed
420 code is printed on the standard output. This option causes this not to be
423 \rare{-U
}{ Set number of diff context lines.
}
425 \rare{-save
\_tmp\_files}{Coccinelle creates some temporary
426 files in
{\tt /tmp
} that it deletes after use. This option causes these
429 \developer{-debug
\_unparsing}{Show some debugging information about the
430 generation of the transformed code. This has the side-effect of
431 deleting the transformed code.
}
433 \developer{-patch
}{ Deprecated option.
}
436 \section{Other options
}
438 \subsection{Version information
}
440 \normal{-version
}{ The version of Coccinelle. No other options are
443 \normal{-date
}{ The date of the current version of Coccinelle. No other
444 options are allowed.
}
448 \minimum{-h, -shorthelp
}{ The most useful commands.
}
450 \minimum{-help, --help, -longhelp
}{ A complete listing of the available
453 \subsection{Controlling the execution of Coccinelle
}
455 \normal{-timeout $
\langle$int$
\rangle$
}{ The maximum time in seconds for
456 processing a single file.
}
458 \rare{-max $
\langle$int$
\rangle$
}{This option informs Coccinelle of the
459 number of instances of Coccinelle that will be run concurrently. This
460 option requires
{\bf -index
}. It is usually used with
{\bf -dir
}.
}
462 \rare{-index $
\langle$int$
\rangle$
}{This option informs Coccinelle of
463 which of the concurrent instances is the current one. This option
464 requires
{\bf -max
}.
}
466 \rare{-mod
\_distrib}{When multiple instances of Coccinelle are run in
467 parallel, normally the first instance processes the first $n$ files, the
468 second instance the second $n$ files, etc. With this option, the files
469 are distributed among the instances in a round-robin fashion.
}
471 \developer{-debugger
}{Option for running Coccinelle from within the OCaml
474 \developer{-profile
}{ Gather timing information about the main Coccinelle
477 \developer{-disable
\_once}{Print various warning messages every time some
478 condition occurs, rather than only once.
}
480 \subsection{Miscellaneous
}
482 \rare{-quiet
}{Suppress most output. This is the default.
}
484 \developer{-pad, -hrule $
\langle$dir$
\rangle$, -xxx, -l1
}{}