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