1FRAMA-C(1) General Commands Manual FRAMA-C(1)
3
7 frama-c[.byte] - a static analyzer for C programs
8 frama-c-gui[.byte] - the graphical interface of frama-c
10
13 frama-c [ options ] files
14
17 frama-c is a suite of tools dedicated to the analysis of source code
18 written in C. It gathers several static analysis techniques in a sin‐
19 gle collaborative framework. This framework can be extended by addi‐
20 tional plugins placed in the $FRAMAC_PLUGIN directory. The command
21 frama-c -help
23 will provide the full list of the plugins that are currently installed.
25 frama-c-gui is the graphical user interface of frama-c. It features
27 the same options as the command-line version.
28 frama-c.byte and frama-c-gui.byte are the ocaml bytecode versions of
30 the command-line and graphical user interface respectively.
31 By default, Frama-C recognizes .c files as C files needing pre-process‐
33 ing and .i files as C files having been already pre-processed. Some
34 plugins may extend the list of recognized files. Pre-processing can be
35 customized through the -cpp-command and -cpp-extra-args options.
36
39 Syntax
40 Options taking an additional parameter can also be written under the
42 form
43 -option=param
45 This option is mandatory when param starts with a dash ('-')
47 Most options that takes no parameter have a corresponding
49 -no-option
51 option which has the opposite effect.
53 Help options
55 -help gives a short usage notice and the list of installed plugins.
57 -kernel-help
59 prints the list of options recognized by Frama-C's kernel
60 -verbose n
62 Sets verbosity level (default is 1). Setting it to 0 will output
63 less progress messages. This level can also be set on a per
64 plugin basis, with option -plugin-verbose n. Verbosity level of
65 the kernel can be controlled with option -kernel-verbose n.
66 Level of debug is controlled by the -debug n option, which has
67 the same per plugin specializations. The default debugging
68 level is 0.
69 -quiet Sets verbosity and debugging level to 0.
71 Options controlling Frama-C's kernel
73 -absolute-valid-range <min-max>
75 considers that all numerical addresses in the range min-max are
76 valid. Bounds are parsed as ocaml integer constants. By default,
77 all numerical adresses are considered invalid.
78 -add-path p1[,p2[...,pn]]
80 adds directories <p1> through <pn> to the list of directories in
81 which plugins are searched
82 [-no]-annot
84 reads ACSL annotation. This is the default. Annotation are not
85 pre-processed by default. Use -pp-annot for that.
86 [-no]-constfold
88 folds all syntactically constant expressions in the code before
89 the analyzes. Defaults to no.
90 [-no]-continue-annot-error
92 When analyzing an annotation, the default behavior (the -no ver‐
93 sion of this option) when a typechecking error occurs is to
94 reject the source file as is the case for typechecking errors
95 within the C code. With this option on, the typechecker will
96 only output a warning and discard the annotation but typecheck‐
97 ing will continue.
98 -cpp-command cmd
100 Uses cmd as the command to pre-process C files. Defaults to the
101 CPP environment variable or to
102 gcc -C -E -I.
104 if it is not set. In order to preserve ACSL annotations, the
106 preprocessor must keep comments (the -E option for gcc).
107 -cpp-extra-args args
109 Gives additional arguments to the pre-processor. This is only
110 useful when -preprocess-annot is set. Pre-processing annotations
111 is done in two separate pre-processing stages. The first one is
112 a normal pass on the C code which retains macro definitions.
113 These are then used in the second pass during which annotations
114 are pre-processed. args are used only for the first pass, so
115 that arguments that should not be used twice (such as additional
116 include directives or macro definitions) must thus go there
117 instead of -cpp-command.
118 [-no]-dynlink
120 When on, load all the dynamic plug-ins found in the search path
121 (see -print-plugin-path for more information on the default
122 search path). Otherwise, only plugins requested by -load-modules
123 will be loaded. Default behavior is on.
124 -float-digits n
126 When outputting floating-point numbers, display n digits.
127 Defaults to 12.
128 -float-flush-to-zero
130 Floating point operations flush to zero
131 -float-hex
133 display floats as hexadecimal
134 -float-relative
136 display float interval as [ lower_bound++width ]
137 -journal-disable
139 Do not output a journal of the current session. See -journal-
140 enable.
141 -journal-enable
143 On by default, dumps a journal of all the actions performed dur‐
144 ing the current Frama-C session in the form of an ocaml script
145 that can be replayed with -load-script. The name of the script
146 can be set with the -journal-name option.
147 -journal-name name
149 Set the name of the journal file (without the .ml extension).
150 Defaults to frama_c_journal.
151 [-no]-keep-comments
153 Tries to preserve comments when pretty-printing the source code
154 (defaults to no).
155 [-no]-keep-switch
157 When -simplify-cfg is set, keeps switch statements. Defaults to
158 no.
159 [-no]-lib-entry
161 Indicates that the entry point is called during program execu‐
162 tion. This implies in particular that global variables can not
163 be assumed to have their initial values. The default is -no-lib-
164 entry: the entry point is also the starting point of the program
165 and globals have their initial value.
166 -load file
168 load the (previously saved) state contained in file.
169 -load-module m1[,m2[...,mn]]
171 loads the ocaml modules <m1>through <mn>. These modules must be
172 .cmxsfiles for the native code version of Frama-c and
173 .cmoor.cmafiles for the bytecode version (see the Dynlink sec‐
174 tion of Ocaml manual for more information). All modules which
175 are present in the plugin search paths are automatically loaded.
176 -load-script s1[,s2,[...,sn]]
178 loads the ocaml scripts <s1> through <sn>. The scripts must be
179 .mlfiles. They must be compilable relying only on Ocaml stan‐
180 dard library and Frama-C's API. If some custom compilation step
181 is needed, compile them outside of Frama-C and use -load-module
182 instead.
183 -machdep machine
185 uses machine as the current machine-dependent configuration
186 (size of the various integer types, endiandness, ...). The list
187 of currently supported machines is available through -machdep
188 help option.
189 -main f
191 Sets f as the entry point of the analysis. Defaults to 'main'.
192 By default, it is considered as the starting point of the pro‐
193 gram under analysis. Use -lib-entry if f is supposed to be
194 called in the middle of an execution.
195 -obfuscate
197 prints an obfuscated version of the code (where original identi‐
198 fiers are replaced by meaningless one) and exits. The correspon‐
199 dance table between original and new symbols is kept at the
200 beginning of the result.
201 -ocode file
203 redirects pretty-printed code to file instead of standard out‐
204 put.
205 [-no]-orig-name
207 During the normalization phase, some variables may get renamed
208 when different variable with the same name can co-exist (e.g. a
209 global variable and a formal parameter). When this option is on,
210 a message is printed each time this occurs. Defaults to no.
211 [-no]-overflow
213 arithmetic operations may overflow (this is the default option).
214 The -no-overflow version assumes that the result of all arith‐
215 metic operations is within the bounds of the associated type.
216 [-no]-pp-annot
218 pre-process annotations. This is currently only possible when
219 using gcc (or GNU cpp) pre-processor. The default is to not pre-
220 process annotations.
221 [-no]-print
223 pretty-prints the source code as normalized by CIL (defaults to
224 no).
225 -print-libpath
227 outputs the directory where Frama-C kernel library is installed
228 -print-path
230 alias of -print-share-path
231 -print-plugin-path
233 outputs the directory where Frama-C searchs its plugins (can be
234 overidden by the FRAMAC_PLUGIN variable and the -add-path
235 option)
236 -print-share-path
238 outputs the directory where Frama-C stores its data (can be
239 overidden by the FRAMAC_SHARE variable)
240 -safe-arrays
242 For structure fields that are arrays, assumes that all accesses
243 must be in bound (set by default). The opposite option is
244 -unsafe-arrays
245 -save file
247 Saves Frama-C's state into file after the analyzes have taken
248 place.
249 [-no]-simplify-cfg
251 removes break, continue and switch statement before the ana‐
252 lyzes. Defaults to no.
253 -time file
255 outputs user time and date in the given file when Frama-C exits.
256 -typecheck
258 forces typechecking of the source files. This option is only
259 relevant if no further analysis is requested (as typechecking
260 will implicitely occurs before the analysis is launched).
261 -ulevel n
263 syntactically unroll loops n times before the analysis. This can
264 be quite costly and some plugins (e.g. the value analysis) pro‐
265 vide more efficient ways to perform the same thing. See their
266 respective manuals for more information.
267 [-no]-unicode
269 outputs ACSL formulas with utf8 characters. This is the default.
270 When given the -no-unicode option, Frama-C will use the ASCII
271 version instead. See the ACSL manual for the correspondance.
272 -unsafe-arrays
274 see -safe-arrays
275 [-no]-unspecified-access
277 checks the that read/write accesses occuring in unspecified
278 order (according to the C standard's notion of sequence point)
279 are performed on separate locations. This is the default. With
280 -no-unspecified-access , assumes that it is always the case.
281 -version
283 outputs the version string of Frama-C
284 Plugins specific options
286 For each plugin, the command
288 frama-c -plugin-help
290 will give the list of options that are specific to the plugin.
292
295 It is possible to control the places where Frama-C looks for its files
296 through the following variables.
297 FRAMAC_LIB
299 The directory where kernel's compiled interfaces are installed
300 FRAMAC_PLUGIN
302 The directory where Frama-C can find standard plug-ins. If you
303 wish to have plugins in several places, use -add-path instead.
304 FRAMAC_SHARE
306 The directory where Frama-C datas are installed.
307
310 Frama-C homepage, http://frama-c.com
311 2010-04-12 FRAMA-C(1)