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

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>