--- layout: fc_discuss_archives title: Message 12 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, I'm interessed in developing code for data structures like Linked
Lists, Graphs and so on. Is frama-c suitable for that?

2015-04-24 13:18 GMT-03:00 Allberson Dantas <allberson85 at gmail.com>:

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



-- 
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/12894089/attachment-0001.html>