--- layout: fc_discuss_archives title: Message 115 from Frama-C-discuss on September 2013 ---
I don't know where Jessie3 is! No one knows where Jessie3 is! - Claude PS: http://en.wikipedia.org/wiki/Asterix_and_the_Chieftain%27s_Shield On 09/18/2013 02:49 PM, Dragan wrote: > Hi all, > I have installed Z3 version 4.3.1 and > why3config --detect > > Found prover Alt-Ergo version 0.94 (it is an old version that is less > tested than the current one). > Found prover Z3 version 4.3.1, Ok. > Found prover Coq version 8.3pl4, Ok. > Found prover PVS version 6.0, Ok. > 4 provers detected and 0 provers detected with unsupported version > == Found /usr/local/lib/why3/plugins/dimacs.cmxs == > == Found /usr/local/lib/why3/plugins/tptp.cmxs == > == Found /usr/local/lib/why3/plugins/hypothesis_selection.cmxs == > == Found /usr/local/lib/why3/plugins/genequlin.cmxs == > > Perhaps I missed something important in configuration of frama-c and why3 > when I got the following error. > > <mymachine>:~/formal/frama-c-Fluorine-20130601/tests/swap$ frama-c > -jessie3 swap.c swap2.c > [kernel] preprocessing with "gcc -C -E -I. swap.c" > [kernel] preprocessing with "gcc -C -E -I. swap2.c" > [jessie3] failure: Prover Z3,3.2 not installed or not configured > [kernel] Current source was: swap.c:1 > The full backtrace is: > Raised at file "src/kernel/log.ml <http://log.ml>", line 523, > characters 30-31 > Called from file "src/kernel/log.ml <http://log.ml>", line 517, > characters 9-16 > Re-raised at file "src/kernel/log.ml <http://log.ml>", line > 520, characters 15-16 > Called from file "register.ml <http://register.ml>", line 43, > characters 8-80 > Called from file "list.ml <http://list.ml>", line 74, > characters 24-34 > Called from file "register.ml <http://register.ml>", line 59, > characters 4-209 > Called from file "queue.ml <http://queue.ml>", line 134, > characters 6-20 > Called from file "src/kernel/boot.ml <http://boot.ml>", line > 37, characters 4-20 > Called from file "src/kernel/cmdline.ml <http://cmdline.ml>", > line 732, characters 2-9 > Called from file "src/kernel/cmdline.ml <http://cmdline.ml>", > line 212, characters 4-8 > > Plug-in jessie3 aborted: internal error. > Please report as 'crash' at http://bts.frama-c.com/. > Your Frama-C version is Fluorine-20130601. > Note that a version and a backtrace alone often do not contain > enough > information to understand the bug. Guidelines for reporting > bugs are at: > > http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines > > Does nyone can advice ? > Thanks in advance > > > -- > Dragan Stosic > Senior developer at IBM > phone: 085-773-1050 > e-mail: dragan.stosic at gmail.com <mailto:dragan.stosic at gmail.com> > e-mail:DRAGANST at ie.ibm.com <mailto:e-mail%3ADRAGANST at ie.ibm.com> > IBM Technology Campus > Damastown Industrial Estate > Mulhuddart > Dublin 15 > Ireland > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss >