Frama-C-discuss mailing list archives

Emilie.Timbou at continental-corporation.com (Emilie.Timbou at continental-corporation.com) · Wed, 6 May 2009 14:04:03 +0200

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

-- 
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                    |

------------------------------

Message: 3
Date: Tue, 05 May 2009 17:18:58 +0200
From: Claude March? <Claude.Marche at inria.fr>
Subject: Re: [Frama-c-discuss] Generation of invariants
To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr>
Message-ID: <4A0058E2.4000307 at inria.fr>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed

Pascal Cuoq wrote:
> Hello,
> 
> On May 4, 2009, at 12:22 PM, Jonathan-Christofer Demay wrote:
> 
>> Another thing I would be interested in is quite the opposite. Given 
>> a C
>> function, I would like to compute an invariant at a particular point 
>> of
>> a function.
>>
>> I this something that has already been thought of as futur feature of
>> Frama-C ? If not, well then this is something I'm considering working
>> on.
> 
> You may be interested in Yannick Moy's article at VMCAI 2008,

A more recent and more detailed reference than "eir" VMCAI paper is 
"eir" thesis:

http://www.lri.fr/~marche/moy09phd.pdf

> [1] http://en.wikipedia.org/wiki/Spivak_pronoun

-- 
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
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 6
**********************************************

-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? enlev?e...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090506/6f388874/attachment.htm 

Frama-C-discuss mailing list archives

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