--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on June 2012 ---
Hi Virgile, thank you for you hint. I have run the following command: $ frama-c -wp -wp-out /c/Temp -wp-rte -wp-trace -wp-proof alt-ergo /c/src/wp.c and provide the resulting content of /c/Temp as attached file. Maybe can somebody make out of what is going wrong? What mean the different kind of files (body.txt, ergo.txt, ergo.txt, head.why) and how are they combined for calling the theorem prover? Thanks, Sylvain -------------- next part -------------- A non-text attachment was scrubbed... Name: Temp.zip Type: application/zip Size: 9535 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120626/71b15f5b/attachment.zip>