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


mantis:frama-c:jessie

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

mantis:frama-c:jessie [2012/05/16 15:31]
yakobowski created by moving content from main page
mantis:frama-c:jessie [2012/05/16 15:56] (current)
yakobowski Move part from main page.
Line 1: Line 1:
 ====== Jessie ====== ====== Jessie ======
  
-This page presents some information ​about the [[http://​frama-c.com/​jessie.html|Jessie plugin]] of Frama-C.+This page presents some tips about the [[http://​frama-c.com/​jessie.html|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 ===== ===== Known issues =====
mantis/frama-c/jessie.txt · Last modified: 2012/05/16 15:56 by yakobowski