--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on April 2015 ---
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 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] -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150422/13433942/attachment-0001.html>