--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on April 2015 ---
It seems that you have a version of Why3 in /usr/local/bin. I suggest that you remove it manually and reinstall it using opam - Claude -------- Forwarded Message -------- Subject: Jessie umbound symbol problem Date: Mon, 20 Apr 2015 23:14:46 -0300 From: Allberson Dantas <allberson85 at gmail.com> To: frama-c-discuss-owner at lists.gforge.inria.fr I'm on Ubuntu 14.04 and I've installed frama-c / why by opam (4.01.0). I'm running frama-c with jessie but there is this error: $ frama-c -jessie copy.c [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing copy.c (with preprocessing) [jessie] Starting Jessie translation [jessie] Producing Jessie files in subdir copy.jessie [jessie] File copy.jessie/copy.jc written. [jessie] File copy.jessie/copy.cloc written. [jessie] Calling Jessie tool in subdir copy.jessie Generating Why function copy [jessie] Calling VCs generator. why3 ide --extra-config /home/hpe/.opam/4.01.0/lib/why/why3/why3.conf copy.mlw [Config] reading extra configuration file /home/hpe/.opam/4.01.0/lib/why/why3/why3.conf /usr/local/lib/why3/plugins/genequlin can't be loaded : Dynlink error : error loading shared library: /usr/local/lib/why3/plugins/genequlin.cmxs: undefined symbol: camlWhy3__Term__t_app_4489 /usr/local/lib/why3/plugins/tptp can't be loaded : Dynlink error : error loading shared library: /usr/local/lib/why3/plugins/tptp.cmxs: undefined symbol: camlWhy3__Pp__print_list_1023 /usr/local/lib/why3/plugins/hypothesis_selection can't be loaded : Dynlink error : error loading shared library: /usr/local/lib/why3/plugins/hypothesis_selection.cmxs: undefined symbol: camlWhy3__Pp__print_list_1023 [GUI] Init the GTK interface... done. [GUI config] reading icons... done. [GUI] Creating tree model... done [GUI] found regular file 'copy.mlw' [GUI] using 'copy' as directory for the project [GUI session] Opening session... [GUI session] Opening session: update done [GUI session] Opening session: done [GUI session] Adding file '../copy.mlw' [GUI] adding file ../copy.mlw in database Error while reading file '../copy.mlw': File "/home/hpe/.opam/4.01.0/lib/why/why3/jessie_why3.mlw", line 268, characters 13-27: unbound symbol 'Double.div_post' make: ** [why3ide] Erro 1 [jessie] user error: Jessie subprocess failed: make -f copy.makefile why3ide -- Allberson Dantas [Doutorando em Ci?ncia da Computa??o - UFC] [Analista de Sistemas do Serpro - Servi?o Federal de Processamento de Dados]