--- layout: fc_discuss_archives title: Message 70 from Frama-C-discuss on March 2009 ---
Hi everyone, I try to get Jessie running on Windows XP and cygwin. I've installed Frama-C, Z3, and Simplify. When I run Jessie on a test program, I get an error message: ~/progs/fc/swap> frama-c -jessie-analysis swap.c Parsing [preprocessing] running gcc -C -E -I. -include C:\Frama-C\share\frama-c\jessie\jessie_prolog.h -dD swap.c Cleaning unused parts Symbolic link Starting semantical analysis Starting Jessie translation Producing Jessie files in subdir swap.jessie File swap.jessie/swap.jc written. File swap.jessie/swap.cloc written. Calling Jessie tool in subdir swap.jessie Generating Why function Swap Generating Why function main Calling VCs generator. why -simplify [...] why/swap.why Fatal error: exception Sys_error("File exists") make: *** [simplify/swap_why.sx] Error 2 Jessie subprocess failed: make -f swap.makefile simplify Juan Soto reported a similar problem on this list and it was suggested to set some environment variables. If I add export WHYLIB=/cygdrive/c/Frama-C/share/frama-c/why export FRAMAC_SHARE=/cygdrive/c/Frama-C/share/frama-c to my .bashrc, why doesn't find prelude.why: ~/progs/fc/swap> frama-c -jessie-analysis swap.c [...] make: Warning: File `swap.makefile' has modification time 0.09 s in the future why -simplify [...] why/swap.why cannot find prelude file /cygdrive/c/Frama-C/share/frama-c/why\why\prelude.why make: *** [simplify/swap_why.sx] Error 1 Jessie subprocess failed: make -f swap.makefile simplify Setting WHYLIB to C:/Frama-C/share/frama-c/why export WHYLIB=C:/Frama-C/share/frama-c/why as B?rbara Vieira suggested also doesn't work. Any ideas? - Boris