Newer
Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
---
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).