Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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

  • Subject: [Frama-c-discuss] Gwhy returning only failures on proof verification under windows xp
  • From: xavier.kauffmann at gmail.com (xavier kauffmann)
  • Date: Mon, 4 Oct 2010 11:00:11 +0200
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>