Skip site navigation (1)Skip section navigation (2)

FreeBSD Manual Pages

  
 
  

home | help
FRAMA-C(1)		    General Commands Manual		    FRAMA-C(1)

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  sin-
       gle  collaborative  framework.  This framework can be extended by addi-
       tional plugins placed in	the $FRAMAC_PLUGIN directory. The command

	      frama-c --plugins

       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-process-
       ing  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 form is mandatory when param starts	with a dash ('-').

       Most options that take no parameter have	a corresponding

	      -no-option

       option which has	the opposite effect.

       Help options

       -help  gives a short usage notice.

       -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-ver-
	      bose n.

       -debug n
	      Sets debugging level (default is 0, meaning  no  debugging  mes-
	      sages).	This  option has the same per-plugin (and kernel) spe-
	      cializations as -verbose.

       -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]-aggressive-merging
	      merges function definitions modulo renaming. Defaults to no.

       [-no]-allow-duplication
	      allows duplication of small blocks during	normalization of tests
	      and loops.  Otherwise, normalization uses	labels and gotos. Big-
	      ger  blocks  and	blocks with non-trivial	control	flow are never
	      duplicated. Defaults to yes.

       [-no]-annot
	      reads ACSL annotations. This is  the  default.  Annotations  are
	      pre-processed  by	default. Use -no-pp-annot if you don't want to
	      expand macros in annotations.

       -big-ints-hex max
	      integers larger than max are displayed in	 hexadecimal  (by  de-
	      fault, all integers are displayed	in decimal)

       -check performs	integrity  checks  on the internal AST (for developers
	      only).

       [-no]-asm-contracts
	      generates	contracts for assembly code written according to gcc's
	      extended syntax. Defaults	to yes.

       [-no]-asm-contracts-auto-validate
	      automatically  marks  contracts generated	from asm as valid. De-
	      faults to	no.

       -c11   enables (partial)	C11 compatibility, e.g.	typedef	redefinitions.
	      Defaults to no.

       [-no]-collapse-call-cast
	      allows  implicit	cast  between the value	returned by a function
	      and the lvalue it	is assigned to.	Otherwise, a  temporary	 vari-
	      able is used and the cast	is made	explicit. Defaults to yes.

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

       -const-readonly
	      variables	with const qualifier must be actually  constant.   De-
	      faults to	yes. The opposite option is -unsafe-writable.

       [-no]-continue-annot-error
	      When analyzing an	annotation, the	default	behavior (the -no ver-
	      sion of this option) when	a typechecking error occurs is to  re-
	      ject  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 typecheck-
	      ing will continue	(errors	in C code are still fatal, though).

       -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	-C  option  for	 gcc).
	      %1 and %2	 can be	used in	cmd to denote the original source file
	      and the pre-processed file respectively.

       -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 in-
	      stead of -cpp-command.

       [-no]-cpp-gnu-like
	      indicates	that the chosen	preprocessor accepts the same  set  of
	      options as GNU cpp. Defaults depends on the installed preproces-
	      sor at configure time.  See also -pp-annot.

       -custom-annot-char c
	      uses character c for starting ACSL annotations.

       -enums repr
	      Choose the way the representation	of enumerated types is	deter-
	      mined.  frama-c -enums help gives	the list of available options.
	      Default is gcc-enums

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

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

       -float-hex
	      display floats as	hexadecimal.

       -float-normal
	      display floats with the standard OCaml routine.

       -float-relative
	      display float intervals as [ lower_bound++width ].

       [-no]-force-rl-arg-eval
	      forces  right-to-left evaluation order for arguments of function
	      calls. Otherwise the evaluation order is left unspecified, as in
	      the C standard. Defaults to no.

       [-no]-frama-c-stdlib
	      adds -I$FRAMAC_SHARE/libc	 to  the options given to the cpp com-
	      mand.  If	-cpp-gnu-like is not false,  also  adds	 -nostdinc  to
	      prevent  an inconsistent mix of system and Frama-C header	files.
	      Defaults to yes.

       -implicit-function-declaration _action_
	      warns or aborts when a function is called	before it has been de-
	      clared.  _action_	can be one of ignore, warn, or error. Defaults
	      to warn.

       -initialized-padding-locals
	      Implicit initialization of locals	sets padding  bits  to	0.  If
	      false, padding bits are left uninitialized (defaults to yes).

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

       -journal-enable
	      On by default, dumps a journal of	all the	actions	performed dur-
	      ing  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.

       -keep-unused-specified-functions
	      See -remove-unused-specified-functions

       -kernel-log kind:file
	      copies log messages from the  Frama-C's  kernel  to  file.  kind
	      specifies	which kinds of messages	to be copied (e.g. w for warn-
	      ings, e for errors, etc.). See -kernel-help  for	more  details.
	      Can also be set on a per-plugin basis, with option -plugin-log.

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

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

       -load-module m1[,m2[...,mn]]
	      loads  the  ocaml	modules	_m1_ through _mn_.  These modules must
	      be .cmxs files for  the  native  code  version  of  Frama-c  and
	      .cmo or.cma files	for the	bytecode version (see the Dynlink sec-
	      tion of the 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
	      .ml files.   They	 must  be compilable relying only on the 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. Default is x86_32

       -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  pro-
	      gram  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 identi-
	      fiers  are  replaced  by meaningless ones) and exits. The	corre-
	      spondence	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 out-
	      put.

       [-no]-orig-name
	      During the normalization phase, some variables may  get  renamed
	      when different variables 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]-pp-annot
	      pre-processes  annotations. This is currently only possible when
	      using gcc	(or GNU	cpp) pre-processor. The	 default  is  to  pre-
	      process annotations when the default pre-processor is identified
	      as GNU or	GNU-like. See also -cpp-gnu-like

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

       -print-libpath
	      outputs  the  directory  where the Frama-C kernel	library	is in-
	      stalled.

       -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 op-
	      tion)

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

       [-no]-remove-exn
	      transforms throw and try/catch statements	 into  normal  C func-
	      tions. Defaults to no, unless the	input source language  has  an
	      exception	mechanism.

       -remove-projects	p1,...,pn
	      removes  the  given  projects  p1,...,pn.	  @all_but_current re-
	      moves all	projects but the current one.

       -remove-unused-specified-functions
	      keeps function prototypes	that have an  ACSL  specification  but
	      are  not used in the code. This is the default. Functions	having
	      the attribute FRAMAC_BUILTIN are always kept.

       -safe-arrays
	      For multidimensional arrays or arrays  that  are	fields	inside
	      structs,	assumes	that all accesses must be in bound (set	by de-
	      fault). The opposite option is -unsafe-arrays.

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

       -session	s
	      sets s as	the directory in which session files are searched.

       [-no]-set-project-as-default
	      the current project becomes the default one (and so future -then
	      sequences	are applied on it). Defaults to	no.

       [-no]-simplify-cfg
	      removes  break,  continue	and switch statements before analyses.
	      Defaults to no.

       [-no]-simplify-trivial-loops
	      simplifies trivial loops such as do ...  while  (0)  loops.  De-
	      faults to	yes.

       -then  allows  one to compose analyzes: a first run of Frama-C will oc-
	      cur with the options before -then	and a second run will be  done
	      with  the	 options  after	 -then on the current project from the
	      first run.

       -then-last
	      like -then, but the second group of actions is executed  on  the
	      last project created by a	program	transformer.

       -then-on	prj
	      Similar  to  -then  except  that	the second run is performed in
	      project prj.  If no such project exists, Frama-C exits  with  an
	      error.

       -then-replace
	      like -then-last, but also	removes	the previous current project.

       -time file
	      appends 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 implicitly occur 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) pro-
	      vide  more  efficient ways to perform the	same thing.  See their
	      respective manuals for more information. This can	also be	 acti-
	      vated  on	a per-loop basis via the loop pragma unroll <m>	direc-
	      tive. A negative value for n will	inhibit	such pragmas.

       [-no]-ulevel-force
	      ignores UNROLL loop pragmas disabling unrolling.

       [-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 correspondence.

       -unsafe-arrays
	      see -safe-arrays

       [-no]-unspecified-access
	      checks that read/write accesses occurring	in an unspecified  or-
	      der  (according  to  the C standard's notion of sequence points)
	      are performed on separate	locations.   With  -no-unspecified-ac-
	      cess, assumes that it is always the case (this is	the default).

       -version
	      outputs the version string of Frama-C.

       -warn-decimal-float _freq_
	      warns  when  a  floating-point constant cannot be	exactly	repre-
	      sented (e.g. 0.1).  _freq_ can be	one of none, once, or all

       [-no]-warn-signed-downcast
	      generates	alarms when signed downcasts may exceed	 the  destina-
	      tion range (defaults to no).

       [-no]-warn-signed-overflow
	      generates	 alarms	 for signed operations that overflow (defaults
	      to yes).

       [-no]-warn-unsigned-downcast
	      generates	alarms when unsigned downcasts may exceed the destina-
	      tion range (defaults to no).

       [-no]-warn-unsigned-overflow
	      generates	alarms for unsigned operations that overflow (defaults
	      to no).

       Plugin-specific options

       For each	plugin,	the command

	      frama-c -plugin-help

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

EXIT STATUS
       0      Successful execution

       1      Invalid user input

       2      User interruption	(kill or equivalent)

       3      Unimplemented feature

       4 5 6  Internal error

       125    Unknown error

       Exit status greater than	2 can be considered as a bug (or a feature re-
       quest  for  the case of exit status 3) and may be reported on Frama-C's
       BTS (see	below).

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 plugins.	If you
	      wish to have plugins in several places, use -add-path instead.

       FRAMAC_SHARE
	      The directory where Frama-C data (e.g. its version of the	 stan-
	      dard library) is installed.

SEE ALSO
       Frama-C user manual: $FRAMAC_SHARE/manuals/user-manual.pdf

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

       Frama-C BTS: http://bts.frama-c.com

				  2016-11-23			    FRAMA-C(1)

NAME | SYNOPSIS | DESCRIPTION | OPTIONS | EXIT STATUS | ENVIRONMENT VARIABLES | SEE ALSO

Want to link to this manual page? Use this URL:
<https://www.freebsd.org/cgi/man.cgi?query=frama-c&sektion=1&manpath=FreeBSD+12.1-RELEASE+and+Ports>

home | help