--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on May 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie plug-in



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
______________________________________________________________________________________________________
Answer:

Sorry for not using English language, I forgot.

I tried what you tell me and I had another type of error. I am not sure 
whether it was necessary to put the two lines as a result or not.
When I tested the two lines, I get:

When I tested the first line, I get:

However, I put the Coq libraries in the Variable Environment... 
So, I do not understand the problem and I do not find a answer to resolve 
this problem.

Thank for your interest...

Emilie 
-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? enlev?e...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090507/c38f6b83/attachment-0001.htm 
-------------- section suivante --------------
Une pi?ce jointe non texte a ?t? nettoy?e...
Nom: non disponible
Type: image/gif
Taille: 9453 octets
Desc: non disponible
Url: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090507/c38f6b83/attachment-0002.gif 
-------------- section suivante --------------
Une pi?ce jointe non texte a ?t? nettoy?e...
Nom: non disponible
Type: image/gif
Taille: 6933 octets
Desc: non disponible
Url: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090507/c38f6b83/attachment-0003.gif