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

FreeBSD Manual Pages


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

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

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

       frama-c [ options ] files

       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	taking	an  additional parameter can also be written under the


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

       Most options that take no parameter have	a corresponding


       option which has	the opposite effect.

       Help options

       -help  gives a short usage notice.

	      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.

	      merges function definitions modulo renaming. Defaults to no.

	      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.

	      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

	      generates	contracts for assembly code written according to gcc's
	      extended syntax. Defaults	to yes.

	      automatically  marks  contracts generated	from asm as valid. De-
	      faults to	no.

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

	      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.

	      folds  all syntactically constant	expressions in the code	before
	      analyses.	Defaults to no.

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

	      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.

	      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.

	      Floating point operations	flush to zero.

	      display floats as	hexadecimal.

	      display floats with the standard OCaml routine.

	      display float intervals as [ lower_bound++width ].

	      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.

	      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.

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

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

	      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.

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

	      When  -simplify-cfg is set, keeps	switch statements. Defaults to

	      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.

	      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

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

	      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-

	      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.

	      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

	      pretty-prints the	source code as normalized by CIL (defaults  to

	      outputs  the  directory  where the Frama-C kernel	library	is in-

	      alias of -print-share-path

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

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

	      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.

	      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.

	      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.

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

	      removes  break,  continue	and switch statements before analyses.
	      Defaults to no.

	      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.

	      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

	      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.

	      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.

	      ignores UNROLL loop pragmas disabling unrolling.

	      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.

	      see -safe-arrays

	      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).

	      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

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

	      generates	 alarms	 for signed operations that overflow (defaults
	      to yes).

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

	      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.

       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).

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

	      The directory where kernel's compiled interfaces are installed.

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

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

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

       Frama-C homepage:

       Frama-C BTS:

				  2016-11-23			    FRAMA-C(1)


Want to link to this manual page? Use this URL:

home | help