---
layout: clean_page
---
# Jessie

This page presents some tips about the [Jessie
plugin](http://frama-c.com/jessie.html) of Frama-C.

## Extracting proof obligation from a Jessie project

<http://cavale.gforge.enseeiht.fr/files/extract_obligation>  

``` 
usage: extract_obligation -f=funname -o=obligation [-s=solver] sources
Options:
  -s=<solver> or --solver=<solver>  with solver in {coq,smtlib,alt-ergo} (default is coq)
  -f=<fun>    or --function=<fun>   with fun a function in sources
  -o=<obl>    or --obligation=<obl> with obl an obligation associated to the function (the name in available in the frama-c gui with jessie plugin)\\  
```

## Known issues

To submit a bug for the tools of the Why platform, visit
<https://gforge.inria.fr/tracker/?atid=4012&group_id=999&func=browse>

  - **\\sum, \\prod, etc. are not supported by Jessie**  
    See [this
    message](http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-March/000985.html)
    from frama-c-discuss.

<!-- end list -->

  - **Timeout for provers not working under MS-Windows**  
    This is a known issue in Why 2.18 and earlier versions. See [this
    fix](http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2008-December/000301.html).

<!-- end list -->

  - **Code highlighting in gWhy does not work**  
    This may happen when processing DOS-encoded files.  
    Fix: Convert file to unix encoding (C-x RET f undecided-unix in
    Emacs).