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

EXIT STATUS

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

ENVIRONMENT VARIABLES

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

SEE ALSO

557       Frama-C  user  manual:  https://frama-c.com/download/frama-c-user-manu
558       al.pdf
559
560       Frama-C homepage: https://frama-c.com
561
562       Frama-C BTS: https://git.frama-c.com/pub/frama-c/issues
563
564
565
5662021-06-18                                                          FRAMA-C(1)
Impressum