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