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



I'm really grateful to you, Claude. Thanks.

2015-04-22 5:52 GMT-03:00 Claude Marche <Claude.Marche at inria.fr>:

>
> Hi,
>
> In the new release of Why 2.35, the support for use of the former why VC
> generator and the former graphical interface gwhy is completely dropped
> out. In particular the former executables "why" and "gwhy" are not
> compiled and not installed anymore.
>
> It's true that the behavior of option -jessie-atp should be have been
> changed too, sorry about that. Fortunately there is a workaround, as
> described below.
>
> First, let me say that the recommended way to prove a C program with
> Jessie is:
>
> 1) first, discharge VCs using Why3 proof transformations and as many
> provers as possible, using the GUI:
>
> frama-c -jessie f.c
>
> 2) To replay the former proofs in batch mode, use
>
> frama-c -jessie -jessie-atp=why3replay f.c
>
> If for some reason you want to run a single prover on generated VCs,
> then there is a workaround: you can somehow abuse the jessie options as
> follows
>
> frama-c -jessie -jessie-atp=why3ml -jessie-why3-opt="prove -P alt-ergo" f.c
>
> This will not do the same as the former use of -jessie-atp, because Why3
> does automatically split the conjunctions in the goal, so one should do
> instead:
>
> frama-c -jessie -jessie-atp=why3ml -jessie-why3-opt="prove -P alt-ergo
> -a split_goal_wp" f.c
>
> As you can guess, option -jessie-why3-opt allows you to pass any of the
> options supported by Why3. For more advanced use, you should then look
> at the description of all options in Why3's manual.
>
> Finally, note that this "abuse" is not limited to the use of Why3's
> "prove" subcommand. For example, one may produce an HTML dump of the
> session by
>
> frama-c -jessie -jessie-atp=why3ml -jessie-why3-opt="session html" f.c
>
> The dump will be produced in file f.jessie/f/why3session.html
>
> Hope this helps,
>
> - Claude
>
> On 04/22/2015 04:06 AM, Allberson Dantas wrote:
> > 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
> > <mailto: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>
> >     > <mailto: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>
> >     >     <mailto: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>
> >     >     <mailto: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>
> >     >     <mailto: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
> >     <mailto: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
> >     <tel:%2B33%201%2069%2015%2066%2008>
> >     INRIA Saclay - ?le-de-France           |
> >     Universit? Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
> >     F-91405 <http://www.lri.fr/~marche/ F-91405> ORSAY Cedex
> >             |
> >     _______________________________________________
> >     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/20150422/13433942/attachment-0001.html>