--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on September 2010 ---
On mac os it reads "why-config" not "why_config". Jens -----Urspr?ngliche Nachricht----- > Thanks for the pointers, I tried them but got: > Why -config -> It's not why -config, but why_config (this is a separate executable from why itself). > Then I changed the variable JESSIELIBFILES in swap1.jessie/swap1.makefile > $(WHYLIB)\\why\\jessie.why -> $(WHYLIB)/why/jessie.why and tried why -simplify [...] why/swap1.why, I ran into the same error as before. I have been able to reproduce your issue by positioning explicitly the variable JESSIELIBFILES on the command line of the cygwin shell: JESSIELIBFILES=C:\\Frama-C\\lib\\why\\why\\jessie.why frama-c -jessie -jessie-atp simplify file.c When you use / instead, as in JESSIELIBFILES=C:/Frama-C/lib/why/why/jessie.why frama-c -jessie -jessie-atp simplify file.c then the proof obligations are generated (whether they are proved by Simplify is another matter of course). Could you try that on your setting? i.e. JESSIELIBFILES=C:/Programme/TheoremProver/Frama-C/lib/why/why/jessie.why frama-c -jessie -jessie-atp simplify swap1.c Best regards, -- Virgile Prevosto Ing?nieur-Chercheur, CEA, LIST Laboratoire de S?ret? des Logiciels +33/0 1 69 08 82 98 _______________________________________________ Frama-c-discuss mailing list Frama-c-discuss at lists.gforge.inria.fr http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -------------- next part -------------- A non-text attachment was scrubbed... Name: not available Type: application/ms-tnef Size: 3779 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100919/0f02503c/attachment.bin>