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 + frama-c neon-20140301

  • Subject: [Frama-c-discuss] jessie3 + frama-c neon-20140301
  • From: u28616 at hs-harz.de (Christoph Thielecke)
  • Date: Tue, 12 Aug 2014 16:11:18 +0200
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