--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on August 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] jessie3 + frama-c neon-20140301



Hello,

I have a problem to get jessie3 on frama-c neon working (see below).
It claims that it could not find z3 solver (but its installed, removing prover z3 from ~/.why3.conf does also not help.

Any ideas whats wrong in my setup?


My setup:
======
- Ubuntu 14.04
- Z3 [version 4.3.1 - 64 bit] (manuell kompiliert)
- alt-ergo 0.95.2-1build1
- coq 8.4pl3dfsg-1
- coq-theories 8.4pl3dfsg-1
- Why3 platform, version 0.83 (build date: Mon Aug 11 18:23:24 CEST 2014) (manuell kompiliert)
- /usr/local/bin/frama-c --version
Version: Neon-20140301
Compilation date: Sat Aug 9 14:16:12 CEST 2014
Share path: /usr/local/share/frama-c (may be overridden with FRAMAC_SHARE variable)
Library path: /usr/local/lib/frama-c (may be overridden with FRAMAC_LIB variable)
Plug-in paths: /usr/local/lib/frama-c/plugins (may be overridden with FRAMAC_PLUGIN variable)

why3config --detect
Found prover Alt-Ergo version 0.95.2, Ok.
Found prover Z3 version 4.3.1, Ok.
Found prover Coq version 8.4pl3, Ok.
3 provers detected and 0 provers detected with unsupported version
== Found /usr/local/lib/why3/plugins/dimacs.cmxs ==
== Found /usr/local/lib/why3/plugins/hypothesis_selection.cmxs ==
== Found /usr/local/lib/why3/plugins/tptp.cmxs ==
== Found /usr/local/lib/why3/plugins/genequlin.cmxs ==
Save config to /home/crissi/.why3.conf

Program
======
void main()
{
        int N = 10;
        int s = 0;
        int k = 0;

        /*@ requires N >= 0 && s == 0 && k == 0 ;
          @ ensures k == N * N ;
          */
        while (k<N) {

                // @ ensures s >= 0 ;
                s = s+2*k+1;

                // @ ensures k >= 0;
                k = k+1;
        }

}

Log
====
/usr/local/bin/frama-c -jessie3   -debug 1 -jessie3-verbose 3  fv_aufgabe1.c 
[jessie3] Loading Why3 configuration...
[jessie3] Why3 environment loaded.
[jessie3] Loading Why3 theories...
[jessie3] Loading Why3 modules...
[jessie3] Looking up module mach.int.Int32
[jessie3] Looking up module mach.int.Int64
[kernel] preprocessing with "gcc -C -E -I.  fv_aufgabe1.c"
[jessie3] Loading prover drivers...
[jessie3] failure: Prover Z3,3.2 not installed or not configured
[jessie3] failure: Exception raised when loading prover drivers:
                   anomaly: Log.AbortFatal("jessie3")
[kernel] Current source was: fv_aufgabe1.c:1
[kernel] The full backtrace is:
[kernel] Raised at file "src/kernel/log.ml", line 524, characters 30-31
[kernel] Called from file "src/kernel/log.ml", line 518, characters 9-16
[kernel] Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
[kernel] Called from file "register.ml", line 71, characters 6-113
[kernel] Called from file "queue.ml", line 134, characters 6-20
[kernel] Called from file "src/kernel/boot.ml", line 37, characters 4-20
[kernel] Called from file "src/kernel/cmdline.ml", line 735, characters 2-9
[kernel] Called from file "src/kernel/cmdline.ml", line 214, characters 4-8
[kernel] 
[kernel] Plug-in jessie3 aborted: internal error.
[kernel] Please report as 'crash' at http://bts.frama-c.com/.
[kernel] Your Frama-C version is Neon-20140301.
[kernel] Note that a version and a backtrace alone often do not contain enough
[kernel] information to understand the bug. Guidelines for reporting bugs are at:
[kernel] http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines


With best regards

Christoph