--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on May 2009 ---
Sorry, my answer was unclear: calling coq within gwhy *DOES NOT WORK* The proper way to use coq for discharging VCs generated with frama-C/jessie is frama-c -jessie-analysis -jessie-atp coq <file>.c coqide <file>.jessie/coq/<file>_why.v - Claude PS: by the way, please notice that the language for Frama-C public discussion list is english Emilie.Timbou at continental-corporation.com wrote: > Merci pour votre r?ponse... > J'ai test? ce que vous m'avez conseill? mais cela ne fonctionne pas et les > messages d'erreur s'affiche toujours... > Quand vous me dites de passer le param?tre "why-opt --project" sur la > ligne de commande de frama-c, il ne le reconnait pas, j'ai tout de m?me > regarder dans --help pour les ?ventuelles commande qui pourrait s'y > rapprocher, mais effectivement, cette commande n'est pas reconu... > > Dans ce cas, j'attend d'autre propositions de "d?buggage", et merci ? ceux > qui mont r?pondu ... > > Emilie TIMBOU > > > > frama-c-discuss-request at lists.gforge.inria.fr > Envoy? par : frama-c-discuss-bounces at lists.gforge.inria.fr > 06/05/2009 12:00 > Veuillez r?pondre ? > frama-c-discuss at lists.gforge.inria.fr > > > A > frama-c-discuss at lists.gforge.inria.fr > cc > > Objet > Frama-c-discuss Digest, Vol 12, Issue 6 > > > > > > > Send Frama-c-discuss mailing list submissions to > frama-c-discuss at lists.gforge.inria.fr > > To subscribe or unsubscribe via the World Wide Web, visit > > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > or, via email, send a message with subject or body 'help' to > frama-c-discuss-request at lists.gforge.inria.fr > > You can reach the person managing the list at > frama-c-discuss-owner at lists.gforge.inria.fr > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Frama-c-discuss digest..." > > > Today's Topics: > > 1. Re: RE Frama-c-discuss Digest, Vol 12, Issue 4 (Pariente Dillon) > 2. Re: RE Frama-c-discuss Digest, Vol 12, Issue 4 (Claude March?) > 3. Re: Generation of invariants (Claude March?) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Tue, 5 May 2009 14:59:35 +0200 > From: "Pariente Dillon" <Dillon.Pariente at dassault-aviation.com> > Subject: Re: [Frama-c-discuss] RE Frama-c-discuss Digest, Vol 12, > Issue 4 > To: "Frama-C public discussion" > <frama-c-discuss at lists.gforge.inria.fr> > Message-ID: > > <A6FD74D4A6DA4247AD801E3943634063035943C4 at sctex002.st-cloud.dassault-avion.fr> > > Content-Type: text/plain; charset="iso-8859-1" > > ADDENDUM: > Ce qui est d?crit ci-dessous s'applique surtout au message Thread 10 > killed dans l'image ci-dessous. > > Pour ce qui est du message concernant le Thread 9, il doit falloir passer > le param?tre "-why-opt --project" sur la ligne de commande de "frama-c > -jessie-analysis -jessie-gui". Les sp?cialistes de la question sauront > sans doute bien mieux r?pondre ! > > D. > > Ce probl?me appara?t dans l'environnement Cygwin, lorsque > gWhy lance des processus en // pour prouver la m?me Obligation de Preuve > avec deux prouveurs qui [g?n?rent || lisent] les m?mes fichiers > interm?daires (*.why par exemple). > Je n'ai pas investigu? plus avant. Le seul moyen de > contournement consiste ? ne pas lancer les prouveurs incrimin?s en m?me > temps mais en s?quence. > > > ________________________________ > > De : frama-c-discuss-bounces at lists.gforge.inria.fr > [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] De la part de > Emilie.Timbou at continental-corporation.com > Envoy? : mardi 5 mai 2009 14:39 > ? : frama-c-discuss at lists.gforge.inria.fr > Objet : [Frama-c-discuss] RE Frama-c-discuss Digest, Vol > 12, Issue 4 > > > > Bonjour, > Non je ne l'avais pas trouv? en cherchant dans les > historiques... Merci.. > > Par contre, il me reste toujours un probl?me. > > Ce probl?me apparait lorsque je demande au prouveur > Yices(mono) et Coq de s'ex?cuter... Il ne s'?x?cute pas et dans le Bash > Shell je vois ce qui est encadr? en rouge... J'ai essay? de chercher > l'erreur mais je n'arrive pas ? le r?soudre... > > Pouvez vous me conseiller sur cet autre point ? > > Emilie TIMBOU > > > -------------- next part -------------- > An HTML attachment was scrubbed... > URL: > http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090505/3d9564b3/attachment-0001.htm > > -------------- next part -------------- > A non-text attachment was scrubbed... > Name: not available > Type: image/gif > Size: 5572 bytes > Desc: ATT138894.gif > Url : > http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090505/3d9564b3/attachment-0001.gif > > > ------------------------------ > > Message: 2 > Date: Tue, 05 May 2009 16:45:00 +0200 > From: Claude March? <Claude.Marche at inria.fr> > Subject: Re: [Frama-c-discuss] RE Frama-c-discuss Digest, Vol 12, > Issue 4 > To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr> > Message-ID: <4A0050EC.5060702 at inria.fr> > Content-Type: text/plain; charset=ISO-8859-1; format=flowed > > > The Coq column in GWhy interface was an experiment that remainded > available by mistake in Why 2.18 > > The Yices issue was a bug, fixed in future Why 2.19 > > - Claude > > Emilie.Timbou at continental-corporation.com wrote: >> Bonjour, >> Non je ne l'avais pas trouv? en cherchant dans les historiques... > Merci.. >> Par contre, il me reste toujours un probl?me. >> >> Ce probl?me apparait lorsque je demande au prouveur Yices(mono) et Coq >> de s'ex?cuter... Il ne s'?x?cute pas et dans le Bash Shell je vois ce >> qui est encadr? en rouge... J'ai essay? de chercher l'erreur mais je >> n'arrive pas ? le r?soudre... >> >> Pouvez vous me conseiller sur cet autre point ? >> >> Emilie TIMBOU >> >> >> >> >> *frama-c-discuss-request at lists.gforge.inria.fr* >> Envoy? par : frama-c-discuss-bounces at lists.gforge.inria.fr >> >> 05/05/2009 12:00 >> Veuillez r?pondre ? >> frama-c-discuss at lists.gforge.inria.fr >> >> >> >> A >> frama-c-discuss at lists.gforge.inria.fr >> cc >> >> Objet >> Frama-c-discuss Digest, Vol 12, Issue 4 >> >> >> >> >> >> >> >> >> Send Frama-c-discuss mailing list submissions to >> frama-c-discuss at lists.gforge.inria.fr >> >> To subscribe or unsubscribe via the World Wide Web, visit >> >> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss >> or, via email, send a message with subject or body 'help' to >> frama-c-discuss-request at lists.gforge.inria.fr >> >> You can reach the person managing the list at >> frama-c-discuss-owner at lists.gforge.inria.fr >> >> When replying, please edit your Subject line so it is more specific >> than "Re: Contents of Frama-c-discuss digest..." >> >> >> Today's Topics: >> >> 1. Re: jessie plug-in (Benjamin Monate) >> >> >> ---------------------------------------------------------------------- >> >> Message: 1 >> Date: Mon, 04 May 2009 19:52:47 +0200 >> From: Benjamin Monate <benjamin.monate at cea.fr> >> Subject: Re: [Frama-c-discuss] jessie plug-in >> To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr> >> Message-ID: <49FF2B6F.4010703 at cea.fr> >> Content-Type: text/plain; charset=ISO-8859-1; format=flowed >> >> Bonjour, >> >> Avez-vous lu le message : >> > http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2008-December/000301.html > >> qui est mentionn? sur le Wiki de Frama-C ? >> >> Cordialement, >> -- >> | Benjamin Monate >> | Head of Software Safety Lab. CEA-LIST/DRT/DTSI/SOL/LSL | >> >> >> >> >> ------------------------------ >> >> _______________________________________________ >> 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 >> >> End of Frama-c-discuss Digest, Vol 12, Issue 4 >> ********************************************** >> >> >> ------------------------------------------------------------------------ >> >> _______________________________________________ >> 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 > > > ------------------------------------------------------------------------ > > _______________________________________________ > 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 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex |