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

EXIT STATUS

524       0      Successful execution
525
526       1      Invalid user input
527
528       2      User interruption (kill or equivalent)
529
530       3      Unimplemented feature
531
532       4 5 6  Internal error
533
534       125    Unknown error
535
536       Exit statuses greater than 2 can be considered as a bug (or  a  feature
537       request for the case of exit status 3) and may be reported on Frama-C’s
538       BTS (see below).
539

ENVIRONMENT VARIABLES

541       It is possible to control the places where Frama-C looks for its  files
542       through the following variables.
543
544       FRAMAC_LIB
545              The directory where kernel’s compiled interfaces are installed.
546
547       FRAMAC_PLUGIN
548              The  directory  where Frama-C can find standard plugins.  If you
549              wish to have plugins in several places, use -add-path instead.
550
551       FRAMAC_SHARE
552              The directory where Frama-C data (e.g. its version of the  stan‐
553              dard library) is installed.
554

SEE ALSO

556       Frama-C   user   manual:  http://frama-c.com/download/frama-c-user-man
557       ual.pdf
558
559       Frama-C homepage: http://frama-c.com
560
561       Frama-C BTS: http://bts.frama-c.com
562
563
564
565                                  2020-10-07                        FRAMA-C(1)
Impressum