Newer
Older
Andre Maroneze
committed
---
layout: plugin
title: Jessie
Andre Maroneze
committed
key: main
distrib_mode: obsolete
---
## Overview
**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](acsl.html). It uses internally the languages and tools of the
[Why3](http://why3.lri.fr) environment.
The generated verification conditions can be submitted to many external
automatic provers including
[Alt-Ergo](https://alt-ergo.ocamlpro.com/),
[Z3](https://github.com/Z3Prover) and [CVC4](https://cvc4.github.io/).
For more complex situations, interactive theorem provers can be used to
establish validity of VCs. Please look at the
[Jessie](http://krakatoa.lri.fr) web page for more details.
## Usage
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](http://krakatoa.lri.fr) web page. Please read this document for
details on other command-line options, as well as supported and unsupported
features.