SYSTEM WARNING: 'session_name(): Cannot change session name when session is active' in '/home/gitlab-www/dokuwiki/inc/init.php' line 231

SYSTEM WARNING: 'session_set_cookie_params(): Cannot change session cookie parameters when session is active' in '/home/gitlab-www/dokuwiki/inc/init.php' line 232

mantis:frama-c:jessie [Frama-C]

User Tools

  • Logged in as: anonymous (anonymous)
  • Log Out

Site Tools



This page presents some tips about the Jessie plugin of Frama-C.

Extracting proof obligation from a Jessie project

usage: extract_obligation -f=funname -o=obligation [-s=solver] sources
  -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

  • \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