--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on September 2010 ---
Hi, I am not sure whether this solves your issue under Windows, but under Mac OS X it is recommended that one calls "why-config" before frama-c is called the first time. Regards Jens Gerlach -----Urspr?ngliche Nachricht----- Von: frama-c-discuss-bounces at lists.gforge.inria.fr im Auftrag von Hans-Werner Wiesbrock Gesendet: Do 9/16/2010 11:16 An: Frama-C public discussion Betreff: [Frama-c-discuss] Problems with Window Installation of Frama-C Hi, I'm a freshman in Frama-C and tried to install Frama-C (Boron-20100401) under Windows XP. I further installed cygwin and MinGW 5.1.6 for gcc et.al. But when I want to execute: frama-c -jessie -jessie-atp simplify swap1.c where swap1.c is a simple example: /*@ requires \valid(p); requires \valid(q); assigns *p; assigns *q; ensures *p == \old(*q); ensures *q == \old(*p); */ void swap(int* p, int* q) { int const save = *p; *p = *q; *q = save; } I get: (under cygwin) [kernel] preprocessing with "gcc -C -E -I. -dD swap1.c" [jessie] Starting Jessie translation [jessie] Producing Jessie files in subdir swap1.jessie [jessie] File swap1.jessie/swap1.jc written. [jessie] File swap1.jessie/swap1.cloc written. [jessie] Calling Jessie tool in subdir swap1.jessie Generating Why function swap [jessie] Calling VCs generator. why -simplify [...] why/swap1.why Anomaly: Sys_error<"C:\\Programme\\TheoremProver\\Frama-C\\lib\\whywhyjessie.why: No such file... (under dos) ... why -simplify [...] why/swap1.why Der Befehl "WHYLIB" ist entweder falsch geschrieben oder konnte nicht gefunden werden. What did I make wrong and should do instead? Thank you in advance HWW _______________________________________________ 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: 3947 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100916/f2482da9/attachment.bin>