Provided by: why_2.39-2build1_amd64 bug


       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


       frama-c -jessie [options] files


              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

       -d     debugging mode

       -locs  <f> reads source locations from file f

              verify only specified behavior (safety, variant, default or user-defined behavior)

              <why3 command>  (default: ide)

       -v     verbose mode

       -q     quiet mode (default)

       -main  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

       -help  Display this list of options

       --help Display this list of options


       The  tutorial  and  reference  manual  for  jessie  can  be  obtained   at   the   address

                                           October 2016                                 JESSIE(1)