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 complies to some  Frama-C
	      requirements,  such  as accepting	the same set of	options	as GNU
	      cpp,  and	 accepting  architecture-specific  options   such   as
	      -m32/-m64.  Default  values depend on the	installed preprocessor
	      at configure time.  See also -pp-annot.

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

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

       -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-frama-c-compliant is not false, also adds -nostd-
	      inc 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-frama-c-compliant

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

	      expands #include directives in the pretty-printed	CIL  code  for
	      files in the Frama-C standard library (defaults to no).

	      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-12-02			    FRAMA-C(1)


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

home | help