Man Linux: Main Page and Category List

NAME

       frama-c[.byte] - a static analyzer for C programs

       frama-c-gui[.byte] - the graphical interface of frama-c

SYNOPSIS

       frama-c [ options ] files

DESCRIPTION

       frama-c  is  a  suite of tools dedicated to the analysis of source code
       written in C.  It gathers  several  static  analysis  techniques  in  a
       single  collaborative  framework.  This  framework  can  be extended by
       additional plugins placed in the $FRAMAC_PLUGIN directory. The command

              frama-c -help

       will provide the full list of the plugins that are currently installed.

       frama-c-gui  is  the  graphical user interface of frama-c.  It features
       the same options as the command-line version.

       frama-c.byte and frama-c-gui.byte are the ocaml  bytecode  versions  of
       the command-line and graphical user interface respectively.

       By  default,  Frama-C  recognizes  .c  files  as  C  files needing pre-
       processing and .i files as C files having been  already  pre-processed.
       Some  plugins  may  extend the list of recognized files. Pre-processing
       can be customized through the -cpp-command and -cpp-extra-args options.

OPTIONS

       Syntax

       Options  taking  an  additional parameter can also be written under the
       form

              -option=param

       This option is mandatory when param starts with a dash ('-')

       Most options that takes no parameter have a corresponding

              -no-option

       option which has the opposite effect.

       Help options

       -help  gives a short usage notice and the list of installed plugins.

       -kernel-help
              prints the list of options recognized by Frama-C's kernel

       -verbose n
              Sets verbosity level (default is 1). Setting it to 0 will output
              less  progress  messages.  This  level  can also be set on a per
              plugin basis, with option -plugin-verbose n.  Verbosity level of
              the  kernel  can  be  controlled  with option -kernel-verbose n.
              Level of debug is controlled by the -debug n option,  which  has
              the  same  per  plugin  specializations.   The default debugging
              level is 0.

       -quiet Sets verbosity and debugging level to 0.

       Options controlling Frama-C's kernel

       -absolute-valid-range <min-max>
              considers that all numerical addresses in the range min-max  are
              valid. Bounds are parsed as ocaml integer constants. By default,
              all numerical addresses are considered invalid.

       -add-path p1[,p2[...,pn]]
              adds directories <p1> through <pn> to the list of directories in
              which plugins are searched

       [-no]-annot
              reads  ACSL  annotation. This is the default. Annotation are not
              pre-processed by default. Use -pp-annot for that.

       [-no]-constfold
              folds all syntactically constant expressions in the code  before
              the analyzes. Defaults to no.

       [-no]-continue-annot-error
              When  analyzing  an  annotation,  the  default behavior (the -no
              version of this option) when a typechecking error occurs  is  to
              reject  the  source  file as is the case for typechecking errors
              within the C code. With this option  on,  the  typechecker  will
              only   output   a   warning   and  discard  the  annotation  but
              typechecking will continue.

       -cpp-command cmd
              Uses cmd as the command to pre-process C files. Defaults to  the
              CPP environment variable or to

              gcc -C -E -I.

              if  it  is  not  set. In order to preserve ACSL annotations, the
              preprocessor must keep comments (the -E option for gcc).

       -cpp-extra-args args
              Gives additional arguments to the pre-processor.  This  is  only
              useful when -preprocess-annot is set. Pre-processing annotations
              is done in two separate pre-processing stages. The first one  is
              a  normal  pass  on  the C code which retains macro definitions.
              These are then used in the second pass during which  annotations
              are  pre-processed.   args  are used only for the first pass, so
              that arguments that should not be used twice (such as additional
              include  directives  or  macro  definitions)  must thus go there
              instead of -cpp-command.

       [-no]-dynlink
              When on, load all the dynamic plug-ins found in the search  path
              (see  -print-plugin-path  for  more  information  on the default
              search path). Otherwise, only plugins requested by -load-modules
              will be loaded. Default behavior is on.

       -float-digits n
              When   outputting  floating-point  numbers,  display  n  digits.
              Defaults to 12.

       -float-flush-to-zero
              Floating point operations flush to zero

       -float-hex
              display floats as hexadecimal

       -float-relative
              display float interval as [ lower_bound++width ]

       -journal-disable
              Do not output a journal of the current  session.  See  -journal-
              enable.

       -journal-enable
              On  by  default,  dumps  a  journal of all the actions performed
              during the current Frama-C session  in  the  form  of  an  ocaml
              script  that can be replayed with -load-script.  The name of the
              script can be set with the -journal-name option.

       -journal-name name
              Set the name of the journal file (without  the  .ml  extension).
              Defaults to frama_c_journal.

       [-no]-keep-comments
              Tries  to preserve comments when pretty-printing the source code
              (defaults to no).

       [-no]-keep-switch
              When -simplify-cfg is set, keeps switch statements. Defaults  to
              no.

       [-no]-lib-entry
              Indicates   that  the  entry  point  is  called  during  program
              execution. This implies in particular that global variables  can
              not be assumed to have their initial values. The default is -no-
              lib-entry: the entry point is also the  starting  point  of  the
              program and globals have their initial value.

       -load file
              load the (previously saved) state contained in file.

       -load-module m1[,m2[...,mn]]
              loads the ocaml modules <m1>through <mn>.  These modules must be
              .cmxsfiles  for  the  native  code  version   of   Frama-c   and
              .cmoor.cmafiles  for  the  bytecode  version  (see  the  Dynlink
              section of Ocaml manual for more information). All modules which
              are present in the plugin search paths are automatically loaded.

       -load-script s1[,s2,[...,sn]]
              loads the ocaml scripts <s1> through <sn>.  The scripts must  be
              .mlfiles.   They  must  be  compilable  relying  only  on  Ocaml
              standard library and Frama-C's API. If some  custom  compilation
              step  is  needed, compile them outside of Frama-C and use -load-
              module instead.

       -machdep machine
              uses machine  as  the  current  machine-dependent  configuration
              (size  of the various integer types, endiandness, ...). The list
              of currently supported machines is  available  through  -machdep
              help option.

       -main f
              Sets  f  as the entry point of the analysis. Defaults to 'main'.
              By default, it is  considered  as  the  starting  point  of  the
              program  under  analysis.  Use -lib-entry if f is supposed to be
              called in the middle of an execution.

       -obfuscate
              prints  an  obfuscated  version  of  the  code  (where  original
              identifiers  are  replaced  by  meaningless  one) and exits. The
              correspondance table between original and new symbols is kept at
              the beginning of the result.

       -ocode file
              redirects  pretty-printed  code  to  file  instead  of  standard
              output.

       [-no]-orig-name
              During the normalization phase, some variables may  get  renamed
              when  different variable with the same name can co-exist (e.g. a
              global variable and a formal parameter). When this option is on,
              a message is printed each time this occurs.  Defaults to no.

       [-no]-overflow
              arithmetic operations may overflow (this is the default option).
              The  -no-overflow  version  assumes  that  the  result  of   all
              arithmetic  operations  is  within  the bounds of the associated
              type.

       [-no]-pp-annot
              pre-process annotations. This is currently  only  possible  when
              using gcc (or GNU cpp) pre-processor. The default is to not pre-
              process annotations.

       [-no]-print
              pretty-prints the source code as normalized by CIL (defaults  to
              no).

       -print-libpath
              outputs the directory where Frama-C kernel library is installed

       -print-path
              alias of -print-share-path

       -print-plugin-path
              outputs the directory where Frama-C searches its plugins (can be
              overidden  by  the  FRAMAC_PLUGIN  variable  and  the  -add-path
              option)

       -print-share-path
              outputs  the  directory  where  Frama-C  stores its data (can be
              overidden by the FRAMAC_SHARE variable)

       -safe-arrays
              For structure fields that are arrays, assumes that all  accesses
              must  be  in  bound  (set  by  default).  The opposite option is
              -unsafe-arrays

       -save file
              Saves Frama-C's state into file after the  analyzes  have  taken
              place.

       [-no]-simplify-cfg
              removes   break,   continue  and  switch  statement  before  the
              analyzes. Defaults to no.

       -time file
              outputs user time and date in the given file when Frama-C exits.

       -typecheck
              forces  typechecking  of  the  source files. This option is only
              relevant if no further analysis is  requested  (as  typechecking
              will implicitely occurs before the analysis is launched).

       -ulevel n
              syntactically unroll loops n times before the analysis. This can
              be quite costly and some  plugins  (e.g.   the  value  analysis)
              provide  more  efficient  ways  to  perform the same thing.  See
              their respective manuals for more information.

       [-no]-unicode
              outputs ACSL formulas with utf8 characters. This is the default.
              When  given  the  -no-unicode option, Frama-C will use the ASCII
              version instead. See the ACSL manual for the correspondance.

       -unsafe-arrays
              see -safe-arrays

       [-no]-unspecified-access
              checks the that  read/write  accesses  occuring  in  unspecified
              order  (according  to the C standard's notion of sequence point)
              are performed on separate locations.  This  is the default. With
              -no-unspecified-access , assumes that it is always the case.

       -version
              outputs the version string of Frama-C

       Plugins specific options

       For each plugin, the command

              frama-c -plugin-help

       will give the list of options that are specific to the plugin.

ENVIRONMENT VARIABLES

       It  is possible to control the places where Frama-C looks for its files
       through the following variables.

       FRAMAC_LIB
              The directory where kernel's compiled interfaces are installed

       FRAMAC_PLUGIN
              The directory where Frama-C can find standard plug-ins.  If  you
              wish to have plugins in several places, use -add-path instead.

       FRAMAC_SHARE
              The directory where Frama-C datas are installed.

SEE ALSO

       Frama-C homepage, http://frama-c.com

                                  2010-04-12                        FRAMA-C(1)