Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.


[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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


  • Subject: [Frama-c-discuss] Fwd: Jessie umbound symbol problem
  • From: allberson85 at gmail.com (Allberson Dantas)
  • Date: Tue, 21 Apr 2015 15:29:19 -0300
  • In-reply-to: <5535E68D.1010702@inria.fr>
  • References: <CADH2bc9QJgeuRZ1kDV5DMT8xHzqG6K0WpmRGvazU8A8i13m_Ug@mail.gmail.com> <5535E68D.1010702@inria.fr>

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>:

>
> 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]
>
>
> _______________________________________________
> 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/e6f0cbc4/attachment.html>