Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.


[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] using jessie plug-in


  • Subject: [Frama-c-discuss] using jessie plug-in
  • From: gslee at ropas.snu.ac.kr (Gyesik Lee)
  • Date: Fri, 18 Sep 2009 14:03:49 +0900

Dear all,

I am using Frama-C for the first time and wondering if there is a
up-to-date tutorial for jessie plug-in to be combined with Why tool
which is installed together with Frama-C.

I found one on the main web page of Frama-C, but it seems outdated.
In the 1st page it is written to use -jessie-analysis option which
seems to be supported not any more.

And when I just try

frama-c -jessie test.c

then I get the following message

===========
test at user$ frama-c -jessie test.c
[kernel] preprocessing with "gcc -C -E -I.  -dD test.c"
[jessie] Starting Jessie translation
test.c:8:[jessie] failure: Unexpected failure.
                  Please submit bug report (Ref.
"src/jessie/interp.ml:1747:18").
[kernel] Plugin jessie aborted because of an internal error.
         Please report with 'crash' at http://bts.frama-c.com
===========

The test.c file contains the Dijkstra's flag sorting program.

Was something wrong during the installation? (Gut the frama-c-gui can
be launched too.)

(I am using Ubuntu 9.4)

Best,

Gyesik