Warning Jessie is currently not actively maintained and probably incompatible with the latest Frama-C versions.
The Jessie plug-in allows deductive verification of C programs annotated with ACSL. It uses internally the languages and tools of the Why3 environment. The generated verification conditions can be submitted to many external automatic provers including Alt-Ergo, Z3 and CVC4.
For more complex situations, interactive theorem provers can be used to establish validity of VCs. Please look at the Jessie web page for more details.
The plug-in is activated with the following command line:
frama-c -jessie [options] <file>.c
A short manual including a tutorial and reference is available on the Jessie web page. Please read this document for details on other command-line options, as well as supported and unsupported features.