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

[Frama-c-discuss] Gwhy / Jessie only working with cygwin



Hello everybody,

I'm a thesis student working on static analysis and formal methods to verify
security properties on C code.
I've been playing with Frama C a bit and found some of its features very
useful.

I'm currently following the Jessie plugin tutorial and
using Boron-20100401in a windows environment.
I managed to install several provers in windows and tried:

>frama-c -jessie binary-search.i

Gwhy UI is called but when I launch obligation proof it fails.
--Debug trace shows:

Debug: not removing temporary file
'C:\DOCUME~1\XAVIEKAU\LOCALS~1\Temp\gwhy754112_why.why'
oblig : binary_search_ensures_default_po_2
calling Alt-Ergo on C:\DOCUME~1\XAVIEKAU\LOCALS~1\Temp\gwhy086e64_why.why
command line: alt-ergo
C:\DOCUME~1\XAVIEKAU\LOCALS~1\Temp\gwhy086e64_why.why
Output file C:\DOCUME~1\XAVIEKAU\LOCALS~1\Temp\oute5baae:

Debug: not removing temporary file
'C:\DOCUME~1\XAVIEKAU\LOCALS~1\Temp\gwhy086e64_why.why'
oblig : binary_search_ensures_default_po_3
calling Alt-Ergo on C:\DOCUME~1\XAVIEKAU\LOCALS~1\Temp\gwhydc0b25_why.why
command line: alt-ergo
C:\DOCUME~1\XAVIEKAU\LOCALS~1\Temp\gwhydc0b25_why.why
Output file C:\DOCUME~1\XAVIEKAU\LOCALS~1\Temp\outc7c59e:

--whereas with the same command in cygwin the proof obligation works and
debug outputs:
Debug: not removing temporary file
'C:\DOCUME~1\XAVIEKAU\LOCALS~1\Temp\gwhy8dca0c_why.why'
oblig : binary_search_ensures_default_po_2
calling Alt-Ergo on C:\DOCUME~1\XAVIEKAU\LOCALS~1\Temp\gwhyf26952_why.why
command line: alt-ergo
C:\DOCUME~1\XAVIEKAU\LOCALS~1\Temp\gwhyf26952_why.why
Output file C:\DOCUME~1\XAVIEKAU\LOCALS~1\Temp\out06342d:
*File "C:\DOCUME~1\XAVIEKAU\LOCALS~1\Temp\gwhyf26952_why.why", line 957,
characters 1-421:Valid (0.0460)*

Debug: not removing temporary file
'C:\DOCUME~1\XAVIEKAU\LOCALS~1\Temp\gwhyf26952_why.why'
oblig : binary_search_ensures_default_po_3
calling Alt-Ergo on C:\DOCUME~1\XAVIEKAU\LOCALS~1\Temp\gwhy32eec5_why.why
command line: alt-ergo
C:\DOCUME~1\XAVIEKAU\LOCALS~1\Temp\gwhy32eec5_why.why
Output file C:\DOCUME~1\XAVIEKAU\LOCALS~1\Temp\outa0f5e3:
*File "C:\DOCUME~1\XAVIEKAU\LOCALS~1\Temp\gwhy32eec5_why.why", line 957,
characters 1-777:Valid (0.0620)*

Did you come accross this error or do you know why out files are not created
in temp folder when launched from the standard windows console?

Thank you

Xavier Kauffmann
-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? nettoy?e...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100813/e5311050/attachment.htm>