Scroll to navigation

JESSIE(1) User Commands JESSIE(1)

NAME

Jessie - plugin of the Frama-C environment for static analysis of C code. It aims at deductive verification of behavioral properties of the code, specified using the ACSL language.

SYNOPSIS

frama-c -jessie [options] files

OPTIONS

stops after parsing
stops after typing
check only user-defined annotations (i.e. safety is assumed)
stops after call graph and print call graph
stops after generating intermediate Why3 code
debugging mode
<f> reads source locations from file f
verify only specified behavior (safety, variant, default or user-defined behavior)
<why3 command> (default: ide)
verbose mode
quiet mode (default)
main function for interprocedural abstract interpretation (needs -ai <domain>)
fast ai (needs -ai <domain> and -main <function>)
verify inferred annotations (needs -ai <domain>)
apply region-based separation on pointers
treats warnings as errors
prints version and exit
generate vcs for all pointer offsets
verify invariants only (Arguments policy)
verify only these functions

-gen_frame_rule_with_ft Experimental : Generate frame rule for predicates and logic functions using only their definitions

Display this list of options
Display this list of options

SEE ALSO

The tutorial and reference manual for jessie can be obtained at the address http://krakatoa.lri.fr/jessie.html

October 2016