User Tools

  • Logged in as: anonymous (anonymous)
  • Logout

Site Tools


mantis:frama-c:jessie

Jessie

This page presents some tips about the Jessie plugin 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 from frama-c-discuss.
  • Timeout for provers not working under MS-Windows
    This is a known issue in Why 2.18 and earlier versions. See this fix.
  • 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).
mantis/frama-c/jessie.txt · Last modified: 2012/05/16 15:56 by yakobowski