--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on June 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] alt-ergo silently ignored / any idea?



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>