frama-c-gui(1)

NAME

frama-c-gui - Framework for source code analysis of software written in C

SYNOPSIS

frama-c-gui [options] [files...]

DESCRIPTION

This manual page documents briefly the frama-c-gui command.

This manual page was written for the Debian GNU/Linux distribution
because the original program does not have a manual page.

OPTIONS

GENERAL OPTIONS: -version
print version information; -print-path
print Frama-C share path; -no-unicode
do not use utf8 in messages; -save filename
save the state into file [filename] after computations.; -load filename
load an initial (previously saved) state from file [filename].; -time filename
append user time and date to [filename] at exit.; -quiet
do not print results of analyzes on stdout.; -ocode filename
when printing code, redirects the output to file [filename].; -lib-entry
run analysis for an incomplete application e.g. an API call. See
the -main option to set the entry point name.; -main name
set to name the entry point for analysis. Use -lib-entry if this is not for a complete application. Defaults to main; -machdep machine
use [machine] as the current machine dependent configuration. Use
-machdep help to see the list of available machines.; -msvc
switch to MSVC mode. Default mode is gcc.; -debug n
level of debug (defaults to 0).
SYNTACTICAL TOOLS: -print
pretty print original code with its comments.; -simplify-cfg
remove break, continue and switch statement before analyzes.; -keep-switch
keep switch statements despite -simplify-cfg.; -keep-comments
try to keep comments in C code (defaults to false).; -ulevel n
unroll loops n times (defaults to 0) before analyzes.; -constfold
fold all constant expressions in the code before analysis.; -obfuscate
print an obfuscated version of files to standard output and exit.; -metrics
print some metrics on stdout.; -metrics-dump <s>
print some metrics into the specified file.
DYNAMIC (EXPERIMENTAL): -add-path path
add a search path for dynamic plugins; -load-module module
load a module dynamically; -dynamic-debug sub-options
use '-dynamic-debug -help' to get information about sub-options
FILES: -cpp-command CPP
CPP string is used to build the preprocessing command.

Defaults to $CPP environment variable or else "gcc -C -E -I."

If unset, the command is built as follow:

CPP -o <preprocessed file> <source file>

%1 and %2 can be used into CPP string to mark the position of
<source file> and <preprocessed file> respectively.; -cpp-extra-args
additional arguments passed to the preprocessor while preprocessing the C code but not while preprocessing annotations.; -no-annot
do not read annotation.; -pp-annot
pre-process annotations (if they are read).; -warn-unspecified-order
warns for side effects occuring in unspecified order (default:
false); -files-debug sub-options
use '-files-debug -help' to get information about sub-options
MEMZONES (EXPERIMENTAL): -memzones
force memzones display (undocumented)
OCCURRENCE: -occurrence
print results of occurrence analysis; -occurrence-debug sub-options
use '-occurrence-debug -help' to get information about sub-options
CALLGRAPH: -cg FILENAME
dump a stratified call graph to FILENAME in dot format; -cg-init-func FUNCTION
use this function as a root service (you can add as many functions as you want; if no function is declared, then root services are
initialized with functions with no callers)
VALUE ANALYSIS: -val
force values computations; -mem-exec name
do not unroll calls to function name (experimental); -mem-exec-all
(experimental); -memory-footprint n
tell the analyser to compromise towards speed or towards low memory use. 1 : small memory; 2 : medium (suitable for recent notebooks);
3 : big (suitable for workstations with 3Gb physical memory or
more). Defaults to 2.; -float-digits n
display this number of digits when printing floats. Defaults to 4.; -propagate-top
do not stop value analysis even if state is degenerating; -plevel n
use n as the precision level for arrays accesses. Array accesses
are precise as long as the interval for the index contains less
than n values. (defaults to 200); -slevel n
use n as number of path to explore in parallel EXPERIMENTAL
(defaults to 0); -wlevel n
set n as number of iterations before widening (defaults to 3); -absolute-valid-range min-max
min and max must be integers in decimal, hexadecimal (0x, 0X),
octal (0o) or binary (0b) notation and hold in 64 bits. Assume that that all absolute addresses outside of this range are invalid.
Without this option all absolute addresses are assumed to be
invalid.; -context-depth n
use n as the depth of the default context for value analyses.
(defaults to 2); -context-width n
use n as the width of the default context for value analyses.
(defaults to 2); -context-valid-pointers
context generation will only allocate valid pointers until the
-context-depth and then use NULL (defaults to false); -no-overflow
assume that arithmetic operations never overflow; -no-unspecified-access
assume that all read/write accesses occuring in unspecified order
are separated (defaults to false); -unsafe-arrays
do not assume that accesses to arrays are in bounds.; -val-debug sub-options
use '-val-debug -help' to get information about sub-options
FUNCTIONAL DEPENDENCIES: -deps
force dependencies display; -calldeps
force callsite-wise dependencies (through value analysis)
USERS: -users
compute users (through value analysis)
SEMANTIC CONSTANT FOLDING: -semantic-const-folding
force semantic constant propagation and pretty print the new source code.; -semantic-const-fold f1,...,fn
propagate constants only into functions f1,...,fn.; -cast-from-constant
allow introduction of new casts from a folded constant.
INOUT (EXPERIMENTAL): -inout
force operational inout display; this gives the operational inputs, an over-approximation of the set of locations whose initial value
is used; and the sure outputs, an under-approximation of the set of writen tsets; -out
force internal out display; this is an over-approximation of the
set of written tsets; -deref
force deref display (undocumented); -access_path
force the access path information to be computed; -input
force display of operational inputs computed in a linear pass.
Locals and function parameters are not displayed; -input_with_formals
force display of operational inputs computed in a linear pass.
Function parameters are displayed, locals are not.
SEMANTIC CALLGRAPH: -scg-dump
dump the semantic call graph to stdout
SECURITY (EXPERIMENTAL): -security-analysis
perform security analysis; -security-no-annotation
do not recognize security annotations; -security-annotation <s>
recognize security annotations of the specified lattice; -security-lattice <s>
specify security lattice; -security-propagate-assertions
propagate security assertions when possible; -security-slicing
perfom the security slicing analysis; -security-debug sub-options
use '-security-debug -help' to get information about sub-options
IMPACT (EXPERIMENTAL): -impact-pragma f1,...,fn
use the impact pragmas in the code of functions f1,...,fn

//@impact pragma expr <expr_desc>; : impact of the value from the
next statement (not yet implemented)

//@impact pragma stmt; : impact of the next statement; -impact-print
print the impacted stmt
C TO JESSIE (EXPERIMENTAL): -jessie-analysis
perform C to Jessie translation; -jessie-project-name <s>
specify project name for Jessie analysis; -jessie-gui
call graphical interface after Jessie analysis; -jessie-int-model <s>
set the model for integer arithmetic (exact, bounded or modulo); -jessie-behavior <s>
restrict verification to a specific behavior (safety, default or a user-defined behavior); -jessie-gen-only
only generates jessie code (for developer use); -jessie-gen-goals
generates WHY goals instead of calling an automatic prover; -jessie-no-regions
do not separate memory into regions (for developer use); -jessie-no-prolog
do not include Jessie prolog (for developer use); -jessie-std-stubs
use annotated standard headers; -jessie-hint-level <i>
level of hints, i.e. assertions to help the proof (e.g. for string usage); -jessie-infer-annot <s>
infer function annotations (inv, pre, spre, wpre); -jessie-abstract-domain <s>
use specified abstract domain (box, oct or poly); -jessie-atp <s>
use specified automated theorem prover (alt-ergo, cvcl, harvey,
simplify, yices, z3, zenon); -jessie-cpu-limit <i>
set the time limit in sec. for the analysis; -jc-opt <s>
give an option to Jc (e.g., -trust-ai); -why-opt <s>
give an option to Why (e.g., -fast-wp)
PROGRAM DEPENDENCE GRAPH (EXPERIMENTAL): -pdg-debug sub-options
use '-pdg-debug -help' to get information about sub-options
SPARE CODE (EXPERIMENTAL): -sparecode-analysis
perform a spare code analysis; -sparecode-no-annot
don't select more things to keep every reachable annotation; -rm-unused-globals
only remove unused global types and variables (automatically done
by -sparecode-analysis)
SLICING: -slice-print
pretty print the sliced code; -slice-undef-functions
allow the use of the -slicing-level option for calls to undefined
functions; -no-slice-undef-functions
by default, don't slice the prototype of undefined functions; -slicing-level n
set the default level of slicing used to propagate to the calls

0 : don't slice the called functions

1 : don't slice the called functions but propagate the marks anyway

2 : try to use existing slices, create at most one

3 : most precise slices

note: this value (defaults to 2) is not used for calls to undefined functions

except when '-slice-undef-functions' option is set.; -slice-assert f1,...,fn
select the assertions of functions f1,...,fn; -slice-calls f1,...,fn
select every calls to functions f1,...,fn, and all their effect; -slice-loop-inv f1,...,fn
select the loop invariants of functions f1,...,fn; -slice-loop-var f1,...,fn
select the loop variants of functions f1,...,fn; -slice-pragma f1,...,fn
use the slicing pragmas in the code of functions f1,...,fn as
slicing criteria

//@slice pragma ctrl; : to reach this control-flow point

//@slice pragma expr <expr_desc;> : to preserve the value of an
expression at this control-flow point

//@slice pragma stmt; : to preserve the effect of the next
statement; -slice-return f1,...,fn
select the result (returned value) of functions f1,...,fn; -slice-threat f1,...,fn
select the threats of functions f1,...,fn; -slice-value v1,...,vn
select the result of left-values v1,...,vn at the end of the
function given as entry point

(addresses are evaluated at the beginning of the function given as entry point); -slice-rd v1,...,vn
select the read accesses to left-values v1,...,vn

(addresses are evaluated at the beginning of the function given as entry point); -slice-wr v1,...,vn
select the write accesses to left-values v1,...,vn

(addresses are evaluated at the beginning of the function given as entry point); -slicing-debug sub-options
use '-slicing-debug -help' to get information about sub-options
AORAI (AKA LTL_TO_ACSL -- EXPERIMENTAL): -ltl <s>
Specifies file name for LTL property; -to-buchi <s>
Only generates the buchi automata (in Promela language) in file
's'.; -buchi <s>
Considers the property described by the buchi automata (in Promela language) from file 's'.; -ltl-verbose
Gives some information during computation.; -show-op-spec
Displays computed pre and post-condition of each operation.; -output-c-file <s>
Specifies generated file name for annotated C code; -ltl-dot
Generates a dot file of the Buchi automata.; -ltl-AI-off
Does not use abstract interpretation; -ltl-advance-AI-off
Does not use advance abstract interpretation
VALVIEWER: -monospace-font f
use font f as monospace font (defaults to Monospace,Lucida Sans
Unicode,Sans); -general-font f
use font f as general font (defaults to Helvetica,Lucida Sans
Unicode,Sans)
PROJECT: -project-debug sub-options
use '-project-debug -help' to get information about sub-options
JOURNALIZATION: -journal-disable
do not output any journal; -journal-name
set the filename of the journal (do not write any extension)
JOURNAL LOADING: -load-journal filename
file name of the journal to load
HELP: -help
Display this list of options; --help
Display this list of options

LICENSE

This manual page was written by Mehdi Dogguy dogguy@pps.jussieu.fr for the Debian GNU/Linux system (but may be used by others). Permission is granted to copy, distribute and/or modify this document under the terms of the GNU Lesser General Public License, Version 2.1 or any later
version published by the Free Software Foundation; considering as
source code all the file that enable the production of this manpage.

AUTHOR

Mehdi Dogguy <<dogguy@pps.jussieu.fr>>

docs.sk

comprehensive documentation repository

Most Viewed