1FRAMA-C(1)                                                          FRAMA-C(1)
2
3
4

NAME

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

SYNOPSIS

11       frama-c [ options ] files
12

DESCRIPTION

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

OPTIONS

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

EXIT STATUS

516       0      Successful execution
517
518       1      Invalid user input
519
520       2      User interruption (kill or equivalent)
521
522       3      Unimplemented feature
523
524       4 5 6  Internal error
525
526       125    Unknown error
527
528       Exit  statuses  greater than 2 can be considered as a bug (or a feature
529       request for the case of exit status 3) and may be reported on Frama-C’s
530       BTS (see below).
531

ENVIRONMENT VARIABLES

533       It  is possible to control the places where Frama-C looks for its files
534       through the following variables.
535
536       FRAMAC_LIB
537              The directory where kernel’s compiled interfaces are installed.
538
539       FRAMAC_SHARE
540              The directory where Frama-C data (e.g. its version of the  stan‐
541              dard library) is installed.
542

SEE ALSO

544       Frama-C  user  manual:  https://frama-c.com/download/frama-c-user-manu
545       al.pdf
546
547       Frama-C homepage: https://frama-c.com
548
549       Frama-C BTS: https://git.frama-c.com/pub/frama-c/issues
550
551
552
5532021-06-18                                                          FRAMA-C(1)
Impressum