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



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                    |