Linux Certif

Toute la documentation sur la certification Linux LPI

frama-c-gui.byte

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.

SEE ALSO

frama-c-gui (1) frama-c (1)

AUTHOR

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

COPYRIGHT

Copyright © 2009 Mehdi Dogguy