FreeBSD Manual Pages
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-frama-c-compliant 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. [-no]-autoload-plugins 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. -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-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. -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-frama-c-compliant [-no]-print pretty-prints the source code as normalized by CIL (defaults to no). [-no]-print-libc expands #include directives in the pretty-printed CIL code for files in the Frama-C standard library (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-12-02 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-gui&sektion=1&manpath=FreeBSD+12.2-RELEASE+and+Ports>