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: dragan.stosic at gmail.com (Dragan)
  • Date: Wed, 18 Sep 2013 13:49:16 +0100
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", line 523, characters 30-31
         Called from file "src/kernel/log.ml", line 517, characters 9-16
         Re-raised at file "src/kernel/log.ml", line 520, characters 15-16
         Called from file "register.ml", line 43, characters 8-80
         Called from file "list.ml", line 74, characters 24-34
         Called from file "register.ml", line 59, characters 4-209
         Called from file "queue.ml", line 134, characters 6-20
         Called from file "src/kernel/boot.ml", line 37, characters 4-20
         Called from file "src/kernel/cmdline.ml", line 732, characters 2-9
         Called from file "src/kernel/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
e-mail:DRAGANST at ie.ibm.com
IBM Technology Campus
Damastown Industrial Estate
Mulhuddart
Dublin 15
Ireland
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130918/ef622cc7/attachment.html>