--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on April 2015 ---
Thanks Claude. I've used now a fresh ubuntu version of 14.04 and the instalation succeded for the gui mode. But, in the batch mode it comes this error: $ frama-c -jessie -jessie-atp alt-ergo 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. why -alt-ergo [...] why/copy.why /bin/sh: 1: why: not found make: ** [why/copy_why.why] Erro 127 [jessie] user error: Jessie subprocess failed: make -f copy.makefile alt-ergo Do you have an idea of what I'm doing wrong? Thanks a lot again. 2015-04-21 18:46 GMT-03:00 Claude Marche <Claude.Marche at inria.fr>: > > why3 config --detect > > On 04/21/2015 08:29 PM, Allberson Dantas wrote: > > Thank you again, Claude. I've removed all why/why3/frama-c stuff and > > I've installed them again from opam. But, now comes 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 : > > cannot find file /usr/local/lib/why3/plugins/genequlin.cmxs in search > path > > /usr/local/lib/why3/plugins/tptp can't be loaded : Dynlink error : > > cannot find file /usr/local/lib/why3/plugins/tptp.cmxs in search path > > /usr/local/lib/why3/plugins/hypothesis_selection can't be loaded : > > Dynlink error : cannot find file > > /usr/local/lib/why3/plugins/hypothesis_selection.cmxs in search path > > [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 "copy/../copy.mlw", line 3, characters 0-18: > > Library file not found: int > > make: ** [why3ide] Erro 1 > > [jessie] user error: Jessie subprocess failed: make -f copy.makefile > why3ide > > > > > > 2015-04-21 2:56 GMT-03:00 Claude Marche <Claude.Marche at inria.fr > > <mailto:Claude.Marche at inria.fr>>: > > > > > > 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 > > <mailto:allberson85 at gmail.com>> > > To: frama-c-discuss-owner at lists.gforge.inria.fr > > <mailto: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] > > > > > > _______________________________________________ > > Frama-c-discuss mailing list > > Frama-c-discuss at lists.gforge.inria.fr > > <mailto:Frama-c-discuss at lists.gforge.inria.fr> > > > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > > > > > > > > > > -- > > Allberson Dantas > > > > [Doutorando em Ci?ncia da Computa??o - UFC] > > [Analista de Sistemas do Serpro - Servi?o Federal de Processamento de > Dados] > > > > > > _______________________________________________ > > Frama-c-discuss mailing list > > Frama-c-discuss at lists.gforge.inria.fr > > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > > > > -- > Claude March? | tel: +33 1 69 15 66 08 > INRIA Saclay - ?le-de-France | > Universit? Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ > F-91405 ORSAY Cedex | > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > -- Allberson Dantas [Doutorando em Ci?ncia da Computa??o - UFC] [Analista de Sistemas do Serpro - Servi?o Federal de Processamento de Dados] -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150421/f7ad572f/attachment-0001.html>