--- layout: fc_discuss_archives title: Message 26 from Frama-C-discuss on September 2010 ---
Hello, Le jeu. 16 sept. 2010 12:36:30 CEST, "Hans-Werner Wiesbrock" <Hans-Werner.Wiesbrock at itpower.de> a ?crit : > 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