--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on October 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Gwhy returning only failures on proof verification under windows xp



Hello,

I also had this problem a while ago

frama-c -jessie -jessie-atp alt-ergo afile.c

returning only failed verifications under gwhy

** The problem does not occur however when using cygwin.**

Did you try using cygwin?
The solution I have currently to launch verifications with jessie and gwhy
from the windows command line is:

* first to preprocess the file afile.c to afile.i using any preprocessor
(visual studio cl.exe works ok if you are using windows)
* change dos eol to unix eol (according to the mailing list some gui
problems occur in gwhy if the wrong eol are used
* call from windows command line cygwin with a "call_bash_framac.sh" script
to launch jessie from cygwin

cmd /c C:\"Program Files"\"Microsoft Visual Studio
8"\Common7\Tools\vsvars32.bat & cl /C /E /I. "afile.c" > "afile.i"
cmd /c dos2unix "afile.i"
cmd /c c:\cygwin\bin\bash.exe -l call_bash_framac.sh afile.i

call_bash_framac.sh only has one line:
frama-c -jessie $1

This works for me.
-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? nettoy?e...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20101004/a872db77/attachment.htm>