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



Claude, do you know how to increase Timeout for Jessie VC's?

$ frama-c -jessie -jessie-atp=why3ml -jessie-why3-opt="prove -P simplify"
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 prove -P simplify --extra-config
/home/allberson/.opam/4.01.0/lib/why/why3/why3.conf copy.mlw
[Config] reading extra configuration file
/home/allberson/.opam/4.01.0/lib/why/why3/why3.conf
copy.mlw Jessie_program WP_parameter copy_ensures_default : Timeout (4.98s)
copy.mlw Jessie_program WP_parameter copy_safety : Timeout (4.99s)


2015-04-22 10:37 GMT-03:00 Allberson Dantas <allberson85 at gmail.com>:

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



-- 
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/20150424/371888c3/attachment-0001.html>