--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on August 2010 ---
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>