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 / Jessie only working with cygwin

  • Subject: [Frama-c-discuss] Gwhy / Jessie only working with cygwin
  • From: xavier.kauffmann at gmail.com (xavier kauffmann)
  • Date: Fri, 13 Aug 2010 15:48:10 +0200
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>