--- layout: fc_discuss_archives title: Message 8 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



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>