--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on April 2015 ---
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>