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] Jessie3 detecting issue Z3,3.2

  • Subject: [Frama-c-discuss] Jessie3 detecting issue Z3,3.2
  • From: Claude.Marche at inria.fr (Claude Marche)
  • Date: Wed, 18 Sep 2013 15:11:52 +0200
  • In-reply-to: <CAOGRM5Zs6HFhqBwpKqM1XMTso4KnWpMu5gXE6jkf39g=21j0TQ@mail.gmail.com>
  • References: <CAOGRM5Zs6HFhqBwpKqM1XMTso4KnWpMu5gXE6jkf39g=21j0TQ@mail.gmail.com>
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
>