--- layout: fc_discuss_archives title: Message 115 from Frama-C-discuss on September 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie3 detecting issue Z3,3.2



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
>