Frama-C-discuss mailing list archives

Claude.Marche at inria.fr (Claude Marché) · Wed, 06 May 2009 14:18:36 +0200

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                    |

Frama-C-discuss mailing list archives

[Frama-c-discuss] RE Frama-c-discuss Digest, Vol 12, Issue 6