1
2
3FRAMA-C(1)                  General Commands Manual                 FRAMA-C(1)
4
5
6

NAME

8       frama-c[.byte] - a static analyzer for C programs
9
10       frama-c-gui[.byte] - the graphical interface of frama-c
11

SYNOPSIS

13       frama-c [ options ] files
14

DESCRIPTION

16       frama-c  is  a  suite of tools dedicated to the analysis of source code
17       written in C.  It gathers several analysis techniques in a single  col‐
18       laborative  framework.   This  framework  can be extended by additional
19       plugins placed in the $FRAMAC_PLUGIN directory.  The command
20
21              frama-c --plugins
22
23       will provide the full list of the plugins that are currently installed.
24
25       frama-c-gui is the graphical user interface of  frama-c.   It  features
26       the same options as the command-line version.
27
28       frama-c.byte  and  frama-c-gui.byte  are the OCaml bytecode versions of
29       the command-line and graphical user interface respectively.
30
31       By default, Frama-C recognizes .c files as C files needing pre-process‐
32       ing  and  .i  files as C files having been already pre-processed.  Some
33       plugins may extend the list of recognized files.  Pre-processing can be
34       customized through the -cpp-command and -cpp-extra-args options.
35

OPTIONS

37   Syntax
38       Options  taking  an  additional parameter can also be written under the
39       form
40
41              -option=param
42
43       This form is mandatory when param starts with a dash (`-').
44
45       Most options that take no parameter have a corresponding
46
47              -no-option
48
49       option which has the opposite effect.
50
51   Help options
52       -help  gives a short usage notice.
53
54       -kernel-help
55              prints the list of options recognized by Frama-C's kernel
56
57       -verbose n
58              sets verbosity level.  Defaults to 1.  Setting it to 0 will out‐
59              put  less  progress  messages.   This level can also be set on a
60              per-plugin basis,  with  option  -plugin-verbose  n.   Verbosity
61              level  of  the kernel can be controlled with option -kernel-ver‐
62              bose n.
63
64       -debug n
65              sets debugging level.  Defaults to 0, meaning no debugging  mes‐
66              sages.   This  option  has the same per-plugin (and kernel) spe‐
67              cializations as -verbose.
68
69       -quiet sets verbosity and debugging level to 0.
70
71   Options controlling Frama-C's kernel
72       -absolute-valid-range min-max
73              considers that all numerical addresses in the range min-max  are
74              valid.   Bounds  are  parsed  as  OCaml  integer  constants.  By
75              default, all numerical addresses are considered invalid.
76
77       -add-path p1[,p2[...,pn]]
78              adds directories p1 through pn to the  list  of  directories  in
79              which plugins are searched.
80
81       [-no]-aggressive-merging
82              merges function definitions modulo renaming.  Defaults to no.
83
84       [-no]-allow-duplication
85              allows duplication of small blocks during normalization of tests
86              and loops.  Otherwise,  normalization  uses  labels  and  gotos.
87              Bigger blocks and blocks with non-trivial control flow are never
88              duplicated.  Defaults to yes.
89
90       [-no]-annot
91              reads ACSL annotations.  This is the default.   Annotations  are
92              pre-processed by default.  Use -no-pp-annot if you don't want to
93              expand macros in annotations.
94
95       -big-ints-hex max
96              integers larger  than  max  are  displayed  in  hexadecimal  (by
97              default, all integers are displayed in decimal).
98
99       -check performs  integrity  checks  on the internal AST (for developers
100              only).
101
102       [-no]-asm-contracts
103              generates contracts for assembly code written according to gcc's
104              extended syntax.  Defaults to yes.
105
106       [-no]-asm-contracts-auto-validate
107              automatically  marks  contracts  generated  from  asm  as valid.
108              Defaults to no.
109
110       -c11   enables (partial) C11 compatibility, e.g. typedef redefinitions.
111              Defaults to no.
112
113       [-no]-collapse-call-cast
114              allows  implicit  cast  between the value returned by a function
115              and the lvalue it is assigned to.  Otherwise, a temporary  vari‐
116              able is used and the cast is made explicit.  Defaults to yes.
117
118       [-no]-constfold
119              folds  all syntactically constant expressions in the code before
120              analyses.  Defaults to no.
121
122       -const-readonly
123              variables  with  const  qualifier  must  be  actually  constant.
124              Defaults to yes.  The opposite option is -unsafe-writable.
125
126       [-no]-continue-annot-error
127              when analyzing an annotation, the default behavior (the -no ver‐
128              sion of this option) when a  typechecking  error  occurs  is  to
129              reject  the  source  file as is the case for typechecking errors
130              within the C code.  With this option on,  the  typechecker  will
131              only output a warning and discard the annotation but type‐check‐
132              ing will continue (errors in C code are still fatal, though).
133       Deprecated: use -kernel-warn-abort=-annot-error instead.
134
135       -cpp-command cmd
136              uses cmd as the command to pre-process C files.  Defaults to the
137              CPP environment variable or to
138
139              gcc -C -E -I.
140
141       if it is not set.  If unset, the command is built as follows:
142
143              CPP -o
144
145       %1  and %2 can be used into the CPP string to mark the position of  and
146       respectively.  Note that  this  option  is  often  better  replaced  by
147       -cpp-extra-args.
148
149       -cpp-extra-args args
150              gives additional arguments to the pre-processor.  Pre-processing
151              annotations is done in two separate pre-processing stages.   The
152              first  one  is  a  normal pass on the C code which retains macro
153              definitions.  These are then used  in  the  second  pass  during
154              which annotations are pre-processed.  args are used only for the
155              first pass, so that arguments that  should  not  be  used  twice
156              (such  as  additional  include  directives or macro definitions)
157              must thus go there instead of -cpp-command.
158
159       [-no]-cpp-frama-c-compliant
160              indicates that the chosen preprocessor complies to some  Frama-C
161              requirements,  such  as accepting the same set of options as GNU
162              cpp,  and  accepting  architecture-specific  options   such   as
163              -m32/-m64.   Default values depend on the installed preprocessor
164              at configure time.  See also -pp-annot.
165
166       [-no]-autoload-plugins
167              when on, load all the dynamic plugins found in the  search  path
168              (see  -print-plugin-path  for  more  information  on the default
169              search path).  Otherwise, only plugins requested by -load-module
170              will be loaded.  Defaults to on.
171
172       -enums repr
173              choose  the way the representation of enumerated types is deter‐
174              mined.  frama-c -enums help gives the list of available options.
175              Default is gcc-enums.
176
177       -float-digits n
178              when   outputting  floating-point  numbers,  display  n  digits.
179              Defaults to 12.
180
181       -float-flush-to-zero
182              floating point operations flush to zero.
183
184       -float-hex
185              display floats as hexadecimal.
186
187       -float-normal
188              display floats with the standard OCaml routine.
189
190       -float-relative
191              display float intervals as [ lower_bound++width ].
192
193       [-no]-frama-c-stdlib
194              adds -I$FRAMAC_SHARE/libc to the options given to the  cpp  com‐
195              mand.  If -cpp-frama-c-compliant is not false, also adds -nostd‐
196              inc to prevent an inconsistent mix of system and Frama-C  header
197              files.  Defaults to yes.
198
199       -implicit-function-declaration action
200              warns  or  aborts  when  a function is called before it has been
201              declared.   action  can  be  one  of  ignore,  warn,  or  error.
202              Defaults to warn.
203       Deprecated:  use  -kernel-warn-key typing:implicit-function-declaration
204       instead.
205
206       -initialized-padding-locals
207              implicit initialization of locals sets padding bits  to  0.   If
208              false, padding bits are left uninitialized.  Defaults to yes.
209
210       -inline-calls f1,...,fn
211              syntactically  inlines  calls to functions f1,...,fn.  Recursive
212              functions are inlined only at the first level.  Calls via  func‐
213              tion pointers are not inlined.
214
215       -journal-disable
216              do  not  output  a  journal  of the current session.  See -jour‐
217              nal-enable.
218
219       -journal-enable
220              on by default, dumps a journal of all the actions performed dur‐
221              ing  the  current Frama-C session in the form of an OCaml script
222              that can be replayed with -load-script.  The name of the  script
223              can be set with the -journal-name option.
224
225       -journal-name name
226              sets  the  name of the journal file (without the .ml extension).
227              Defaults to frama_c_journal.
228
229       -json-compilation-database path
230              use   path    as    a    JSON    compilation    database    (see
231              <https://clang.llvm.org/docs/JSONCompilationDatabase.html>   for
232              more  information):  each  file  preprocessed  by  Frama-C  will
233              include  corresponding -I and -D flags according to the specifi‐
234              cations in path.   If  path  is  a  directory,  use  <path>/com‐
235              pile_commands.json.   Disabled by default.  Note: this option is
236              only available if Frama-C was compiled with yojson support.
237
238       [-no]-keep-comments
239              tries to preserve comments when pretty-printing the source code.
240              Defaults to no.
241
242       [-no]-keep-switch
243              when -simplify-cfg is set, keeps switch statements.  Defaults to
244              no.
245
246       -keep-unused-specified-functions
247              see -remove-unused-specified-functions.
248
249       -kernel-log kind:file
250              copies log messages from the Frama-C's  kernel  to  file.   kind
251              specifies  which  kinds  of  messages  to be copied (e.g.  w for
252              warnings, e  for  errors,  etc.).   See  -kernel-help  for  more
253              details.   Can  also  be  set on a per-plugin basis, with option
254              -<plugin>-log.
255
256       -kernel-msg-key k1,...,kn
257              controls the emission of  messages  based  on  categories.   Use
258              -kernel-msg-key  help to get a list of available categories, and
259              -kernel-msg-key=“*” to control all  categories.   To  disable  a
260              category,  add a - before its name; to enable a category, simply
261              add its name, with an optional + before it.  For instance, -ker‐
262              nel-msg-key=-k1,k2  will  disable  messages from category k1 and
263              enable those from category k2.  Can also be set on a  per-plugin
264              basis, with option -<plugin>-msg-key.  Note that each plugin has
265              its own set of categories.
266
267       Options -kernel-warn-<action> below follow  the  same  rules  as  -ker‐
268       nel-msg-key.   Message  categories  and warning categories may have the
269       same name, but they are independent from  each  other.   Warning  cate‐
270       gories  can  also  be  set  on a per-plugin basis, with options -<plug‐
271       in>-warn-<action>.
272
273       For the first three options, a negative form (-k1) will lead k1 to gen‐
274       erate warnings, while for -kernel-warn-key, it will disable category k1
275       entirely (no related message will be emitted).
276
277       -kernel-warn-abort k1,...,kn
278              warning categories k1,...,kn abort the execution.
279
280       -kernel-warn-error k1,...,kn
281              warning categories k1,...,kn change Frama-C's exit status.
282
283       -kernel-warn-feedback k1,...,kn
284              warning categories k1,...,kn produce only a feedback message.
285
286       -kernel-warn-key k1,...,kn
287              warning categories k1,...,kn generate warnings.
288
289       Finally, there are three variants of the options  above  which  emit  a
290       single  message per category: -kernel-warn-err-once, -kernel-warn-feed‐
291       back-once, and -kernel-warn-once.
292
293       [-no]-lib-entry
294              indicates that the entry point is called during  program  execu‐
295              tion.   This  implies in particular that global variables cannot
296              be assumed  to  have  their  initial  values.   The  default  is
297              -no-lib-entry: the entry point is also the starting point of the
298              program and globals have their initial value.
299
300       -load file
301              loads the (previously saved) state contained in file.
302
303       -load-module SPEC
304              dynamically load OCaml plug-ins, modules and scripts.  Each SPEC
305              can  be  an  OCaml source or object file, with or without exten‐
306              sion, or a Findlib package.   Loading  order  is  preserved  and
307              additional dependencies can be listed in *.depend files.
308
309       -load-script SPEC
310              alias for option -load-module.
311
312       -machdep machine
313              uses  machine  as  the  current  machine-dependent configuration
314              (size of the various integer types, endiandness, ...).  The list
315              of  currently  supported  machines  is  available through option
316              -machdep help.  Default is x86_32.
317
318       -main f
319              sets f as the entry point of the analysis.   Defaults  to  main.
320              By  default,  it is considered as the starting point of the pro‐
321              gram under analysis.  Use -lib-entry if  f  is  supposed  to  be
322              called in the middle of an execution.
323
324       -obfuscate
325              prints an obfuscated version of the code (where original identi‐
326              fiers are replaced by meaningless ones) and exits.   The  corre‐
327              spondence  table between original and new symbols is kept at the
328              beginning of the result.
329
330       -ocode file
331              redirects pretty-printed code to file instead of  standard  out‐
332              put.
333
334       [-no]-orig-name
335              During  the  normalization phase, some variables may get renamed
336              when different variables with the same name can co-exist (e.g. a
337              global  variable  and  a formal parameter).  When this option is
338              on, a message is printed each time this occurs.  Defaults to no.
339
340       [-no]-pp-annot
341              pre-processes annotations.  This is currently only possible when
342              using  gcc  (or  GNU  cpp)  pre-processor.   The  default  is to
343              pre-process annotations when the default pre-processor is  iden‐
344              tified as GNU or GNU-like.  See also -cpp-frama-c-compliant.
345
346       [-no]-print
347              pretty-prints the source code as normalized by CIL.  Defaults to
348              no.
349
350       [-no]-print-libc
351              expands #include directives in the pretty-printed CIL  code  for
352              files in the Frama-C standard library.  Defaults to no.
353
354       -print-libpath
355              outputs  the  directory  where  the  Frama-C  kernel  library is
356              installed.
357
358       -print-path
359              alias of -print-share-path.
360
361       -print-plugin-path
362              outputs the directory where Frama-C searches its plugins (can be
363              overridden  by  the  FRAMAC_PLUGIN  variable  and  the -add-path
364              option).
365
366       -print-share-path
367              outputs the directory where Frama-C  stores  its  data  (can  be
368              overridden by the FRAMAC_SHARE variable).
369
370       [-no]-remove-exn
371              transforms  throw  and  try/catch statements into normal C func‐
372              tions.  Defaults to no, unless the input source language has  an
373              exception mechanism.
374
375       -remove-projects p1,...,pn
376              removes  the given projects p1,...,pn.  @all_but_current removes
377              all projects but the current one.
378
379       -remove-unused-specified-functions
380              keeps function prototypes that have an  ACSL  specification  but
381              are  not used in the code.  This is the default.  Functions hav‐
382              ing the attribute FRAMAC_BUILTIN are always kept.
383
384       -safe-arrays
385              for multidimensional arrays or arrays  that  are  fields  inside
386              structs,  assumes  that  all  accesses  must be in bound (set by
387              default).  The opposite option is -unsafe-arrays.
388
389       -save file
390              saves Frama-C's state into file after analyses have taken place.
391
392       -session s
393              sets s as the directory in which session files are searched.
394
395       [-no]-set-project-as-default
396              the current project becomes the default one (and so future -then
397              sequences are applied on it).  Defaults to no.
398
399       [-no]-simplify-cfg
400              removes  break,  continue and switch statements before analyses.
401              Defaults to no.
402
403       [-no]-simplify-trivial-loops
404              simplifies trivial  loops  such  as  do  ...  while  (0)  loops.
405              Defaults to yes.
406
407       -then  allows  one  to  compose  analyses:  a first run of Frama-C will
408              occur with the options before -then and a  second  run  will  be
409              done  with  the  options after -then on the current project from
410              the first run.
411
412       -then-last
413              like -then, but the second group of actions is executed  on  the
414              last project created by a program transformer.
415
416       -then-on prj
417              similar  to  -then  except  that  the second run is performed in
418              project prj.  If no such project exists, Frama-C exits  with  an
419              error.
420
421       -then-replace
422              like -then-last, but also removes the previous current project.
423
424       -time file
425              appends user time and date in the given file when Frama-C exits.
426
427       -typecheck
428              forces  typechecking  of  the source files.  This option is only
429              relevant if no further analysis is  requested  (as  typechecking
430              will implicitly occur before the analysis is launched).
431
432       -ulevel n
433              syntactically  unroll  loops  n times before the analysis.  This
434              can be quite costly and some  plugins  (e.g. Eva)  provide  more
435              efficient  ways to perform the same thing.  See their respective
436              manuals for more information.  This can also be activated  on  a
437              per-loop  basis  via the loop pragma unroll  directive.  A nega‐
438              tive value for n will inhibit such pragmas.
439
440       [-no]-ulevel-force
441              ignores UNROLL loop pragmas disabling unrolling.
442
443       [-no]-unicode outputs ACSL formulas with UTF-8 characters.  This is the
444       default.  When given the -no-unicode option, Frama-C will use the ASCII
445       version instead.  See the ACSL manual for the correspondence.
446
447       -unsafe-arrays
448              see -safe-arrays.
449
450       [-no]-unspecified-access
451              checks that read/write  accesses  occurring  in  an  unspecified
452              order  (according to the C standard's notion of sequence points)
453              are  performed  on  separate   locations.    With   -no-unspeci‐
454              fied-access,  assumes  that  it  is always the case (this is the
455              default).
456
457       -version
458              outputs the version string of Frama-C.
459
460       -warn-decimal-float freq
461              warns when a floating-point constant cannot  be  exactly  repre‐
462              sented (e.g. 0.1).  freq can be one of none, once, or all.
463       Deprecated:  use  -kernel-warn-once parser:decimal-float (and variants)
464       instead.
465
466       [-no]-warn-signed-downcast
467              generates alarms when signed downcasts may exceed  the  destina‐
468              tion range.  Defaults to no.
469
470       [-no]-warn-signed-overflow
471              generates  alarms for signed operations that overflow.  Defaults
472              to yes.
473
474       [-no]-warn-unsigned-downcast
475              generates alarms when unsigned downcasts may exceed the destina‐
476              tion range.  Defaults to no.
477
478       [-no]-warn-unsigned-overflow
479              generates   alarms   for   unsigned  operations  that  overflow.
480              Defaults to no.
481
482   Plugin-specific options
483       For each plugin, the command
484
485              frama-c -plugin-help
486
487       will give the list of options that are specific to the plugin.
488

EXIT STATUS

490       0      Successful execution
491
492       1      Invalid user input
493
494       2      User interruption (kill or equivalent)
495
496       3      Unimplemented feature
497
498       4 5 6  Internal error
499
500       125    Unknown error
501
502       Exit statuses greater than 2 can be considered as a bug (or  a  feature
503       request for the case of exit status 3) and may be reported on Frama-C's
504       BTS (see below).
505

ENVIRONMENT VARIABLES

507       It is possible to control the places where Frama-C looks for its  files
508       through the following variables.
509
510       FRAMAC_LIB
511              The directory where kernel's compiled interfaces are installed.
512
513       FRAMAC_PLUGIN
514              The  directory  where Frama-C can find standard plugins.  If you
515              wish to have plugins in several places, use -add-path instead.
516
517       FRAMAC_SHARE
518              The directory where Frama-C data (e.g. its version of the  stan‐
519              dard library) is installed.
520

SEE ALSO

522       Frama-C   user   manual:  http://frama-c.com/download/frama-c-user-man
523       ual.pdf
524
525       Frama-C homepage: http://frama-c.com
526
527       Frama-C BTS: http://bts.frama-c.com
528
529
530
531                                  2018-01-17                        FRAMA-C(1)
Impressum