Provided by: why_2.39-2build1_amd64 
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
-parse-only
stops after parsing
-type-only
stops after typing
-user-annot-only
check only user-defined annotations (i.e. safety is assumed)
-print-call-graph
stops after call graph and print call graph
-gen-only
stops after generating intermediate Why3 code
-d debugging mode
-locs <f> reads source locations from file f
-behavior
verify only specified behavior (safety, variant, default or user-defined behavior)
-why3cmd
<why3 command> (default: ide)
-v verbose mode
-q quiet mode (default)
-main main function for interprocedural abstract interpretation (needs -ai <domain>)
-fast-ai
fast ai (needs -ai <domain> and -main <function>)
-trust-ai
verify inferred annotations (needs -ai <domain>)
-separation
apply region-based separation on pointers
--werror
treats warnings as errors
--version
prints version and exit
-all-offsets
generate vcs for all pointer offsets
-invariants-only
verify invariants only (Arguments policy)
-verify
verify only these functions
-gen_frame_rule_with_ft Experimental : Generate frame rule for predicates and logic functions using only
their definitions
-help Display this list of options
--help 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 JESSIE(1)