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

[Frama-c-discuss] Fwd: Jessie umbound symbol problem



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]